Theorems · Theorem · group theory
div_one
∀ {G : Type u_3} [inst : DivInvOneMonoid G] (a : G), a / 1 = a- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 629 results in Mathlib
- Foundations
- Depth 7 from the axioms, rests on 44 definitions · uses propext
- Assumes
- DivInvOneMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- mul_oneproof · cited by 3,885
- div_eq_mul_invproof · cited by 715
- inv_oneproof · cited by 301
- DivInvOneMonoidstatement and proof · cited by 3
Cited by629
Results whose statement or proof uses this declaration.
- Rat.cast_intCastproof · cited by 74
- NNRat.cast_natCastproof · cited by 31
- norm_inv'proof · cited by 23
- Complex.norm_cpow_eq_rpow_re_of_posproof · cited by 21
- Rat.cast_ofNatproof · cited by 19
- Real.arctan_zeroproof · cited by 17
- Complex.Gamma_add_oneproof · cited by 12
- div_le_selfproof · cited by 12
- one_div_oneproof · cited by 11
- MeasureTheory.Measure.addHaarMeasure_uniqueproof · cited by 9
- Function.hasTemperateGrowth_one_add_norm_sq_rpowproof · cited by 9
- UpperHalfPlane.norm_exp_two_pi_I_lt_oneproof · cited by 7
Showing the 200 most cited of 629.