Theorems · Theorem · group theory
isPointed_iff_support_eq_bot
∀ {G : Type u_1} [inst : AddGroup G] {M : AddSubmonoid G}, M.IsPointed ↔ M.support = ⊥- Defined in
- Mathlib.Algebra.Group.Submonoid.Support
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Quot.sound
- Assumes
- AddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement and proof · cited by 3,232
- AddSubmonoidstatement and proof · cited by 1,178
- neg_zeroproof · cited by 542
- ZeroMemClass.zero_memproof · cited by 162
- AddSubgroup.extproof · cited by 75
- AddSubgroup.mem_botproof · cited by 18
- AddSubmonoid.supportstatement and proof · cited by 8
- AddSubmonoid.IsPointedstatement and proof · cited by 7
- AddSubmonoid.IsPointed.eq_zero_of_mem_of_neg_memproof · cited by 3
- AddSubmonoid.mem_supportproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- AddSubmonoid.IsPointed.of_support_eq_botproof · cited by 0
- AddSubmonoid.IsPointed.support_eq_botproof · cited by 0