structure SubField (K A : Type u) [CommSemiring K] [Semiring A] [Algebra K A] extends Subalgebra K A : Type u

• carrier : Set A
• mul_mem' {a b : A} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• add_mem' {a b : A} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• algebraMap_mem' (r : K) : (algebraMap K A) r ∈ self.carrier
• mul_comm (x y : A) : x ∈ self.carrier → y ∈ self.carrier → x * y = y * x
• inverse (x : A) : x ∈ self.carrier → x ≠ 0 → ∃ y ∈ self.carrier, x * y = 1

theorem SubField.ext {K A : Type u} {inst✝ : CommSemiring K} {inst✝¹ : Semiring A} {inst✝² : Algebra K A} {x y : SubField K A} (carrier : x.carrier = y.carrier) : x = y

noncomputable instance instLESubField (K A : Type u) [CommSemiring K] [Semiring A] [Algebra K A] : LE (SubField K A)

Equations

• instLESubField K A = { le := fun (L1 L2 : SubField K A) => L1.toSubalgebra ≤ L2.toSubalgebra }

noncomputable def IsMaximalSubfield (K A : Type u) [CommSemiring K] [Semiring A] [Algebra K A] (L : SubField K A) : Prop

Equations

• IsMaximalSubfield K A L = ∀ (B : SubField K A), L ≤ B → B = L

instance instNonemptySubFieldOfNontrivial (K A : Type u) [Field K] [Ring A] [Algebra K A] [Nontrivial A] : Nonempty (SubField K A)

noncomputable instance instPartialOrderSubField (K A : Type u) [Field K] [Ring A] [Algebra K A] : PartialOrder (SubField K A)

Equations

• instPartialOrderSubField K A = PartialOrder.mk ⋯

noncomputable instance instSetLikeSubField (K A : Type u) [Field K] [Ring A] [Algebra K A] : SetLike (SubField K A) A

Equations

• instSetLikeSubField K A = { coe := fun (L : SubField K A) => ↑L.toSubalgebra, coe_injective' := ⋯ }

theorem isMax_iff_isMaxSubfield (K A : Type u) [Field K] [Ring A] [Algebra K A] (L : SubField K A) : IsMax L ↔ IsMaximalSubfield K A L

instance instSubringClassSubField (K A : Type u) [Field K] [Ring A] [Algebra K A] : SubringClass (SubField K A) A

@[simp]

theorem SubField.mem_toSubring (K A : Type u) [Field K] [Ring A] [Algebra K A] {L : SubField K A} {a : A} : a ∈ L.toSubring ↔ a ∈ L

theorem SubField.mem_carrier (K A : Type u) [Field K] [Ring A] [Algebra K A] {L : SubField K A} {a : A} : a ∈ L.carrier ↔ a ∈ L

theorem SubField.ext' {K A : Type u} [Field K] [Ring A] [Algebra K A] {L1 L2 : SubField K A} (h : ∀ (x : A), x ∈ L1 ↔ x ∈ L2) : L1 = L2

@[simp]

theorem SubField.coe_toSubalgebra (K A : Type u) [Field K] [Ring A] [Algebra K A] (L : SubField K A) : ↑L.toSubalgebra = ↑L

theorem SubField.toSubalgebra_injective {K A : Type u} [Field K] [Ring A] [Algebra K A] : Function.Injective toSubalgebra

theorem SubField.toSubalgebra_inj (K A : Type u) [Field K] [Ring A] [Algebra K A] {S U : SubField K A} : S.toSubalgebra = U.toSubalgebra ↔ S = U

noncomputable def SubField.toSubalgebra' (K A : Type u) [Field K] [Ring A] [Algebra K A] : SubField K A ↪o Subalgebra K A

Equations

• SubField.toSubalgebra' K A = { toFun := fun (S : SubField K A) => { toSubsemiring := S.toSubsemiring, algebraMap_mem' := ⋯ }, inj' := ⋯, map_rel_iff' := ⋯ }

@[instance 100]

noncomputable instance SubField.algebra' {K A : Type u} [Field K] [Ring A] [Algebra K A] {K' : Type u} [CommRing K'] [SMul K' K] [Algebra K' A] [IsScalarTower K' K A] (S : SubField K A) : Algebra K' ↥S

Equations

• S.algebra' = S.algebra'

noncomputable instance SubField.instAlgebraSubtypeMem (K A : Type u) [Field K] [Ring A] [Algebra K A] (S : SubField K A) : Algebra K ↥S

Equations

• SubField.instAlgebraSubtypeMem K A S = S.algebra'

noncomputable instance SubField.instFieldSubtypeMemSubalgebraOfNontrivial (K A : Type u) [Field K] [Ring A] [Nontrivial A] [Algebra K A] (L : SubField K A) : Field ↥L.toSubalgebra

Equations

• SubField.instFieldSubtypeMemSubalgebraOfNontrivial K A L = Field.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (q : ℚ≥0) => HMul.hMul ↑q) ⋯ ⋯ (fun (a : ℚ) => HMul.hMul ↑a) ⋯

noncomputable instance SubField.instFieldSubtypeMemOfNontrivial (K A : Type u) [Field K] [Ring A] [Nontrivial A] [Algebra K A] (L : SubField K A) : Field ↥L

Equations

• SubField.instFieldSubtypeMemOfNontrivial K A L = inferInstanceAs (Field ↥L.toSubalgebra)

instance SubField.instFiniteDimensionalSubtypeMem (K A : Type u) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] (L : SubField K A) : FiniteDimensional K ↥L

noncomputable instance SubField.instPreorderOfNontrivial (K A : Type u) [Field K] [Ring A] [Nontrivial A] [Algebra K A] : Preorder (SubField K A)

Equations

• SubField.instPreorderOfNontrivial K A = Preorder.mk ⋯ ⋯ ⋯