Theorems · Definition · commutative algebra

Algebra.EssFiniteType.submonoid

(R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          [inst_3 : Algebra.EssFiniteType R S] → Submonoid ↥(Algebra.EssFiniteType.subalgebra R S)

A submonoid of EssFiniteType.subalgebra R S, whose localization is the whole algebra S.

Defined in: Mathlib.RingTheory.EssentialFiniteness
Cited by: 4 results in Mathlib
Foundations: Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing Algebra Algebra.EssFiniteType

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.

CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
Algebra.algebraMapproof · cited by 4,706
Submonoidstatement · cited by 3,086
Subalgebrastatement · cited by 1,353
Submonoid.comapproof · cited by 179
Algebra.EssFiniteTypestatement and proof · cited by 68
IsUnit.submonoidproof · cited by 56
Algebra.EssFiniteType.subalgebrastatement and proof · cited by 5

Cited by4

Results whose statement or proof uses this declaration.

IntermediateField.fg_top_iffproof · cited by 2
Algebra.EssFiniteType.algHom_extproof · cited by 2
Algebra.EssFiniteType.isNoetherianRingproof · cited by 2
Algebra.essFiniteType_iff_exists_subalgebraproof · cited by 1