Theorems · Definition · group theory

AddConstEquiv.equivUnits

{G : Type u_1} → [inst : Add G] → {a : G} → AddConstEquiv G G a a ≃* (AddConstMap G G a a)ˣ

Group equivalence between G ≃+c[a, a] G and the units of G →+c[a, a] G.

Defined in

Mathlib.Algebra.AddConstMap.Equiv

Cited by

4 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Add