Theorems · Theorem · group theory
Submonoid.powers_one
∀ {M : Type u_1} [inst : Monoid M], Submonoid.powers 1 = ⊥- Cited by
- 7 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Bot.botstatement and proof · cited by 4,720
- Monoidstatement and proof · cited by 3,887
- Submonoidstatement · cited by 3,086
- Submonoid.powersstatement · cited by 408
- OneMemClass.one_memproof · cited by 87
- bot_uniqueproof · cited by 57
- Submonoid.powers_leproof · cited by 19
Cited by7
Results whose statement or proof uses this declaration.
- Module.support_eq_empty_iffproof · cited by 5
- Algebra.smoothLocus_eq_univ_iffproof · cited by 3
- RingHom.locally_ofproof · cited by 2
- RingHom.HoldsForLocalizationAway.of_bijectiveproof · cited by 2
- AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_appproof · cited by 2
- AlgebraicGeometry.StructureSheaf.toOpenₗ_top_bijectiveproof · cited by 1
- RingHom.locally_holdsForLocalizationAwayproof · cited by 0