Theorems · Theorem · group theory
AddSubmonoid.single_mem_pi
∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → AddZeroClass (M i)] [inst_1 : DecidableEq ι] {I : Set ι}
{S : (i : ι) → AddSubmonoid (M i)} (i : ι) (x : M i), Pi.single i x ∈ AddSubmonoid.pi I S ↔ i ∈ I → x ∈ S i- Cited by
- 2 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddZeroClassDecidableEq
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.
- Setstatement and proof · cited by 53,352
- AddZeroClassstatement and proof · cited by 1,237
- AddSubmonoidstatement and proof · cited by 1,178
- Pi.singlestatement · cited by 518
- ZeroMemClass.zero_memproof · cited by 162
- AddSubmonoid.pistatement and proof · cited by 20
- Set.update_mem_pi_iff_of_memproof · cited by 5
Cited by2
Results whose statement or proof uses this declaration.
- AddSubmonoid.pi_le_iffproof · cited by 2
- AddSubmonoid.le_comap_single_piproof · cited by 1