Module

AdditiveEquiv.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.AdditiveEquiv

1 declaration indexed from sourceView source ↗

Module documentation

Additive recoding of multiplicative equivalences

Turns a multiplicative group equivalence into the corresponding equivalence between the additive recodings of its source and target.

Imports1

Mathlib.Algebra.Module.Equiv.Basic

Imported by2

def

additiveEquivOfMulEquiv

L22 ↗

LocalFieldTheory.additiveEquivOfMulEquiv

Documentation

Transport a multiplicative equivalence to an additive equivalence.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace LocalFieldTheory
noncomputable section
universe u

Lean source · full declaration

def additiveEquivOfMulEquiv {A B : Type u} [Group A] [Group B] (e : A ≃* B) :
    Additive A ≃+ Additive B where
  toFun := fun a => Additive.ofMul (e (Additive.toMul a))
  invFun := fun b => Additive.ofMul (e.symm (Additive.toMul b))
  left_inv := by
    intro a
    simp
  right_inv := by
    intro b
    simp
  map_add' := by
    intro a b
    ext
    exact e.map_mul _ _

Module documentation

Additive recoding of multiplicative equivalences

Declarations

additiveEquivOfMulEquiv