Theorems · Theorem · group theory

AddSubmonoid.le_comap_single_pi

∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → AddZeroClass (M i)] [inst_1 : DecidableEq ι]
  (S : (i : ι) → AddSubmonoid (M i)) {I : Set ι} {i : ι},
  S i ≤ AddSubmonoid.comap (AddMonoidHom.single M i) (AddSubmonoid.pi I S)

Defined in: Mathlib.Algebra.Group.Submonoid.Operations
Cited by: 1 results in Mathlib
Foundations: Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddZeroClass DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

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
AddMonoidHomstatement · cited by 3,230
AddZeroClassstatement and proof · cited by 1,237
AddSubmonoidstatement and proof · cited by 1,178
AddSubmonoid.comapstatement · cited by 62
AddSubmonoid.pistatement · cited by 20
AddMonoidHom.singlestatement · cited by 19
AddSubmonoid.mem_comapproof · cited by 8
AddSubmonoid.single_mem_piproof · cited by 2

Cited by1

Results whose statement or proof uses this declaration.

AddSubmonoid.iSup_map_single_leproof · cited by 1