Theorems · Theorem · group theory

Submonoid.IsLocalizationMap.pi

∀ {ι : Type u_1} {M : ι → Type u_2} {N : ι → Type u_3} [inst : (i : ι) → CommMonoid (M i)]
  [inst_1 : (i : ι) → CommMonoid (N i)] (S : (i : ι) → Submonoid (M i)) {f : (i : ι) → M i → N i},
  (∀ (i : ι), (S i).IsLocalizationMap (f i)) → (Submonoid.pi Set.univ S).IsLocalizationMap (Pi.map f)

Defined in: Mathlib.GroupTheory.MonoidLocalization.Lemmas
Cited by: 0 results in Mathlib
Foundations: Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommMonoid CommMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Set.univstatement and proof · cited by 3,945
Submonoidstatement and proof · cited by 3,086
CommMonoidstatement and proof · cited by 2,264
Pi.mapstatement and proof · cited by 60
Submonoid.IsLocalizationMapstatement and proof · cited by 19
Submonoid.pistatement and proof · cited by 17
Submonoid.IsLocalizationMap.surjproof · cited by 8
Submonoid.IsLocalizationMap.exists_of_eqproof · cited by 6
Submonoid.IsLocalizationMap.map_unitsproof · cited by 5
Pi.isUnit_iffproof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.