Theorems · Theorem · group theory
mul_one_div_cancel
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a * (1 / a) = 1- Cited by
- 10 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- GroupWithZerostatement and proof · cited by 691
- Ne.isUnitproof · cited by 99
- IsUnit.mul_one_div_cancelproof · cited by 1
Cited by10
Results whose statement or proof uses this declaration.
- PiLp.nnnorm_toLp_constproof · cited by 4
- smoothingFun_apply_of_map_mul_eq_mulproof · cited by 2
- MeasureTheory.eLpNorm_indicator_const₀proof · cited by 1
- MeasureTheory.MemLp.eLpNorm_indicator_norm_ge_leproof · cited by 1
- MeasureTheory.Measure.MeasureDense.of_generateFrom_isSetAlgebra_finiteproof · cited by 1
- smoothingFun_of_map_mul_eq_mulproof · cited by 1
- ModP.mul_ne_zero_of_pow_p_ne_zeroproof · cited by 1
- exists_norm_eq_iInf_of_complete_convexproof · cited by 1
- smoothingFun_of_powMulproof · cited by 0
- Polynomial.bernoulli_generating_functionproof · cited by 0