Theorems · Theorem · commutative algebra

Localization.subalgebra.ofField.congr_simp

∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S S_1 : Submonoid A) (e_S : S = S_1) (hS : S ≤ nonZeroDivisors A)
  [inst_1 : Field K] [inst_2 : Algebra A K] [inst_3 : IsFractionRing A K],
  Localization.subalgebra.ofField K S hS = Localization.subalgebra.ofField K S_1 ⋯

Defined in: Mathlib.RingTheory.Localization.AsSubring
Cited by: 0 results in Mathlib
Foundations: Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing Field Algebra IsFractionRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites8

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
Fieldstatement and proof · cited by 7,404
Submonoidstatement and proof · cited by 3,086
Subalgebrastatement · cited by 1,353
nonZeroDivisorsstatement and proof · cited by 895
IsFractionRingstatement and proof · cited by 738
Localization.subalgebra.ofFieldstatement and proof · cited by 8

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.