Theorems · Theorem · group theory
AddSubmonoid.mem_top
∀ {M : Type u_1} [inst : AddZeroClass M] (x : M), x ∈ ⊤- Defined in
- Mathlib.Algebra.Group.Submonoid.Defs
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
- Assumes
- AddZeroClass
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.
- Top.topstatement · cited by 9,680
- AddZeroClassstatement and proof · cited by 1,237
- AddSubmonoidstatement · cited by 1,178
- Set.mem_univproof · cited by 416
Cited by21
Results whose statement or proof uses this declaration.
- AddSubmonoid.topEquivproof · cited by 4
- AddSubmonoid.eq_top_iff'proof · cited by 3
- AddSubmonoid.subsingleton_iffproof · cited by 2
- AddSubmonoid.induction_of_closure_eq_top_leftproof · cited by 2
- AddSubmonoid.top_prodproof · cited by 2
- AddSubmonoid.prod_topproof · cited by 1
- addIrreducible_subset_of_addSubmonoidClosure_eq_topproof · cited by 1
- AddMonoidAlgebra.freeAlgebra_lift_of_surjective_of_closureproof · cited by 0
- Algebra.GrothendieckAddGroup.mk_sub_mkstatement and proof · cited by 0
- Algebra.GrothendieckAddGroup.neg_mkstatement · cited by 0
- AddSubmonoid.induction_of_closure_eq_top_rightproof · cited by 0
- AddSubmonoid.pi_emptyproof · cited by 0