English
From a Subalgebra S of L, if S is IsField in the sense of containing inverses for nonzero elements, then toIntermediateField' constructs an intermediate field on L.
Русский
Из подалгебры S L, если S является IsField в смысле содержать обратные элементы ненулевых, тогда toIntermediateField' строит промежуточное поле на L.
LaTeX
$$$\text{toIntermediateField'}(S, hS)\text{ defines an } \text{IntermediateField}(K,L)$$$
Lean4
/-- Turn a subalgebra satisfying `IsField` into an intermediate field. -/
def toIntermediateField' (S : Subalgebra K L) (hS : IsField S) : IntermediateField K L :=
S.toIntermediateField fun x hx => by
by_cases hx0 : x = 0
· rw [hx0, inv_zero]
exact S.zero_mem
letI hS' := hS.toField
obtain ⟨y, hy⟩ := hS.mul_inv_cancel (show (⟨x, hx⟩ : S) ≠ 0 from Subtype.coe_ne_coe.1 hx0)
rw [Subtype.ext_iff, S.coe_mul, S.coe_one, Subtype.coe_mk, mul_eq_one_iff_inv_eq₀ hx0] at hy
exact hy.symm ▸ y.2
