Theorems · Definition · commutative algebra
IsLocalization.invSubmonoid
{R : Type u_1} →
[inst : CommRing R] → Submonoid R → (S : Type u_2) → [inst_1 : CommRing S] → [Algebra R S] → Submonoid SThe submonoid of S = M⁻¹R consisting of { 1 / x | x ∈ M }.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- Algebra.algebraMapproof · cited by 4,706
- Submonoidstatement and proof · cited by 3,086
- Submonoid.mapproof · cited by 190
- Submonoid.leftInvproof · cited by 20
Cited by12
Results whose statement or proof uses this declaration.
- IsLocalization.toInvSubmonoidstatement · cited by 11
- IsLocalization.surj''statement · cited by 2
- IsLocalization.toInvSubmonoid_surjectivestatement · cited by 2
- IsLocalization.finiteType_of_monoid_fgproof · cited by 2
- IsLocalization.mul_toInvSubmonoidstatement · cited by 2
- IsLocalization.equivInvSubmonoidstatement · cited by 1
- IsLocalization.toInvSubmonoid_mulstatement · cited by 1
- IsLocalization.span_invSubmonoidstatement and proof · cited by 1
- IsLocalization.mem_invSubmonoid_iff_exists_mk'statement and proof · cited by 0
- IsLocalization.toInvSubmonoid_eq_mk'statement · cited by 0
- IsLocalization.toInvSubmonoid.congr_simpstatement · cited by 0
- IsLocalization.smul_toInvSubmonoidstatement · cited by 0