instIsFractionRingSubtypeMem — Mathlib

English

A valuation subring A of K yields that the subtype of elements of A forms a subring of K which is a fraction ring of A in K.

Русский

Оценочное подкольцо A внутри K порождает структуру, в которой подпольная часть элементов A образует подкольцо K и является поля частных дробей для A.

LaTeX

$$$IsFractionRing\left(\mathrm{Subtype}\{x\in K\mid x\in A\}\; K\right)$$$

Lean4

instance : IsFractionRing A K
    where
  map_units := fun ⟨y, hy⟩ => (Units.mk0 (y : K) fun c => nonZeroDivisors.ne_zero hy <| Subtype.ext c).isUnit
  surj
    z := by
    by_cases h : z = 0; · use (0, 1); simp [h]
    rcases A.mem_or_inv_mem z with hh | hh
    · use (⟨z, hh⟩, 1); simp
    · refine ⟨⟨1, ⟨⟨_, hh⟩, ?_⟩⟩, mul_inv_cancel₀ h⟩
      exact mem_nonZeroDivisors_iff_ne_zero.2 fun c => h (inv_eq_zero.mp (congr_arg Subtype.val c))
  exists_of_eq {a b} h := ⟨1, by ext; simpa using h⟩

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