English
If P is a predicate on elements of adjoin F s that is closed under algebra map, addition, multiplication, and inversion, and holds for generators from s, then P holds for all elements of adjoin F s (formal induction principle).
Русский
Если P — условие на элементы adjoin F s и оно сохраняется при алгебраическом отображении, сложении, умножении и взятии обратного, а также верно на порождающих s, то верно и на всех элементах adjoin F s.
LaTeX
$$$\\text{adjoin\_induction}_{F,s}(p,\\text{mem},\\text{algebraMap},\\text{add},\\text{inv},\\text{mul}) \\,\\Rightarrow \\, \\forall x (h: x \\in adjoin F s),\, p x h.$$$
Lean4
/-- If `E / L / F` and `E / L' / F` are two field extension towers, `L ≃ₐ[F] L'` is an isomorphism
compatible with `E / L` and `E / L'`, then for any subset `S` of `E`, `L(S)` and `L'(S)` are
equal as intermediate fields of `E / F`. -/
theorem restrictScalars_adjoin_of_algEquiv {L L' : Type*} [Field L] [Field L'] [Algebra F L] [Algebra L E]
[Algebra F L'] [Algebra L' E] [IsScalarTower F L E] [IsScalarTower F L' E] (i : L ≃ₐ[F] L')
(hi : algebraMap L E = (algebraMap L' E) ∘ i) (S : Set E) :
(adjoin L S).restrictScalars F = (adjoin L' S).restrictScalars F :=
by
apply_fun toSubfield using (fun K K' h ↦ by ext x; change x ∈ K.toSubfield ↔ x ∈ K'.toSubfield; rw [h])
change Subfield.closure _ = Subfield.closure _
congr
ext x
exact
⟨fun ⟨y, h⟩ ↦ ⟨i y, by rw [← h, hi]; rfl⟩, fun ⟨y, h⟩ ↦
⟨i.symm y, by rw [← h, hi, Function.comp_apply, AlgEquiv.apply_symm_apply]⟩⟩
