instIsFractionRingSubtypeMemSubalgebra

English

If S is a subalgebra of A inside K, then S carries a fraction ring structure with K as its fraction field; i.e., IsFractionRing S K holds.

Русский

Если S является подалгеброй A внутри K, то у S имеется структура поля дробей, причем K является полем дробей S.

LaTeX

$$$$ \text{IsFractionRing } S K $$$$

Lean4

instance (S : Subalgebra A K) : IsFractionRing S K :=
  by
  refine IsFractionRing.of_field S K fun z ↦ ?_
  rcases IsFractionRing.div_surjective (A := A) z with ⟨x, y, _, eq⟩
  exact ⟨algebraMap A S x, algebraMap A S y, eq.symm⟩

Похожие утверждения