Theorems · Theorem · group theory
Units.val_inv_eq_inv_val
∀ {α : Type u} [inst : DivisionMonoid α] (u : αˣ), ↑u⁻¹ = (↑u)⁻¹- Defined in
- Mathlib.Algebra.Group.Units.Defs
- Cited by
- 57 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
- Assumes
- DivisionMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Unitsstatement and proof · cited by 2,804
- Units.valstatement · cited by 1,966
- DivisionMonoidstatement and proof · cited by 201
- Units.mul_invproof · cited by 67
- inv_eq_of_mul_eq_one_rightproof · cited by 15
Cited by57
Results whose statement or proof uses this declaration.
- IsUnit.invproof · cited by 7
- IsUnit.mul_inv_cancelproof · cited by 6
- Units.val_div_eq_div_valproof · cited by 6
- Valuation.subgroups_basisproof · cited by 5
- hasFDerivAt_inv'proof · cited by 3
- CommGroupWithZero.coe_normUnitproof · cited by 3
- MonoidWithZeroHom.mem_valueGroup_iff_of_commproof · cited by 3
- spectrum.mem_resolventSet_of_norm_lt_mulproof · cited by 3
- ZLattice.covolume_div_covolume_eq_relIndexproof · cited by 2
- Valuation.map_eq_one_of_forall_ltproof · cited by 2
- Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_mem_rangeproof · cited by 2
- spectrum.inv₀_mem_iffproof · cited by 2