Theorems · Theorem · group theory

AddEquiv.eq_iff_eq_on_generator

∀ {G : Type u_2} {G' : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] {g : G},
  (∀ (x : G), x ∈ AddSubgroup.zmultiples g) → ∀ (f₁ f₂ : G ≃+ G'), f₁ = f₂ ↔ f₁ g = f₂ g

Two isomorphisms G ≃+ G' of additive groups are equal if and only if they agree on a generator of G.

Defined in

Mathlib.GroupTheory.SpecificGroups.Cyclic

Cited by

0 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Quot.sound

Assumes

AddGroupAddGroup