English
Given an algebra isomorphism f: B ≃ₐ[A] C, IsCyclotomicExtension S A B implies IsCyclotomicExtension S A C.
Русский
Пусть есть изоморфизм A-алгебр f: B ≃ₐ[A] C. Тогда если IsCyclotomicExtension S A B, то IsCyclotomicExtension S A C.
LaTeX
$$$[IsCyclotomicExtension S A B] \\to (f : B \\simeq[A] C) \\Rightarrow IsCyclotomicExtension S A C$$$
Lean4
/-- Given `(f : B ≃ₐ[A] C)`, if `IsCyclotomicExtension S A B` then
`IsCyclotomicExtension S A C`. -/
protected theorem equiv {C : Type*} [CommRing C] [Algebra A C] [h : IsCyclotomicExtension S A B] (f : B ≃ₐ[A] C) :
IsCyclotomicExtension S A C :=
by
letI : Algebra B C := f.toAlgHom.toRingHom.toAlgebra
haveI : IsCyclotomicExtension { 1 } B C := singleton_one_of_algebraMap_bijective f.surjective
haveI : IsScalarTower A B C := IsScalarTower.of_algHom f.toAlgHom
exact (iff_union_singleton_one _ _ _).2 (trans S { 1 } A B C f.injective)
