We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 4aa3a99 commit 8628ccdCopy full SHA for 8628ccd
1 file changed
Mathlib/FieldTheory/IntermediateField/Basic.lean
@@ -552,6 +552,7 @@ noncomputable def equivFieldRange : L ≃ₐ[K] f.fieldRange :=
552
553
end AlgHom
554
555
+variable (K L L') in
556
@[simp]
557
theorem IsScalarTower.toAlgHom_fieldRange [Algebra L L'] [IsScalarTower K L L'] :
558
(IsScalarTower.toAlgHom K L L').fieldRange = Set.range (algebraMap L L') := by
0 commit comments