Commit 2026-05-21 08:11 466d6fa0

View on Github →

refactor(Algebra): replace SemilinearEquivClass.semilinearEquiv by structure-specific coercions (#37944) Remove the coercion from E to SemilinearEquiv assuming SemilinearEquivClass E and given by SemilinearEquivClass.semilinearEquiv. For each concrete type, reimplement this coercion through the relevant structure projection.

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

modified theorem AlgEquiv.toAlgHom_toLinearMap

modified def AlgEquiv.toLinearEquiv

deleted def AlgEquiv.toLinearMap

Modified Mathlib/Algebra/Algebra/Tower.lean

added theorem AlgEquiv.toAlgHom_restrictScalars

added theorem AlgEquiv.toLinearEquiv_restrictScalars

added theorem AlgHom.toLinearMap_restrictScalars

Modified Mathlib/Algebra/Module/Equiv/Basic.lean

modified def LinearEquiv.restrictScalars

Modified Mathlib/Algebra/Module/Equiv/Defs.lean

Modified Mathlib/Analysis/Complex/Basic.lean

modified theorem Complex.conjCLE_coe_toLinearMap

Modified Mathlib/Analysis/Normed/Operator/Banach.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean

Modified Mathlib/LinearAlgebra/Complex/Determinant.lean

modified theorem Complex.det_conjAe

modified theorem Complex.linearEquiv_det_conjAe

Modified Mathlib/LinearAlgebra/Complex/Module.lean

Modified Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean

modified theorem IsSymmetricAlgebra.equiv_symm_comp

Modified Mathlib/NumberTheory/NumberField/Basic.lean

Modified Mathlib/RingTheory/Coalgebra/Equiv.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean

Modified Mathlib/RingTheory/Invariant/Profinite.lean

Modified Mathlib/RingTheory/Smooth/Pi.lean

Modified Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean

Modified Mathlib/RingTheory/TensorProduct/MvPolynomial.lean

Modified Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean

Modified Mathlib/Topology/Algebra/Module/Equiv.lean

added theorem ContinuousLinearEquiv.toLinearMap_toContinuousLinearMap

Modified Mathlib/Topology/Algebra/Module/FiniteDimension.lean