Theorems · Theorem · group theory
map_units_inv
∀ {M : Type u} [inst : Monoid M] {α : Type u_1} [inst_1 : DivisionMonoid α] {F : Type u_2} [inst_2 : FunLike F M α]
[MonoidHomClass F M α] (f : F) (u : Mˣ), f ↑u⁻¹ = (f ↑u)⁻¹- Defined in
- Mathlib.Algebra.Group.Units.Hom
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Monoidstatement and proof · cited by 3,887
- Unitsstatement and proof · cited by 2,804
- FunLikestatement and proof · cited by 2,560
- Units.valstatement · cited by 1,966
- MonoidHom.compproof · cited by 469
- MonoidHomClass.toMonoidHomproof · cited by 294
- MonoidHomClassstatement and proof · cited by 244
- DivisionMonoidstatement and proof · cited by 201
- Units.coeHomproof · cited by 44
- MonoidHom.map_invproof · cited by 16
Cited by5
Results whose statement or proof uses this declaration.
- IsDiscreteValuationRing.exists_lift_of_le_oneproof · cited by 2
- IsFractionRing.isInteger_of_isUnit_denproof · cited by 2
- LocalSubring.exists_valuationRing_of_isMaxproof · cited by 2
- NumberField.IsCMField.unitsComplexConj_torsionproof · cited by 1
- LocalSubring.exists_le_valuationSubring_of_isIntegrallyClosedInproof · cited by 1