Theorem IsSymmetricAlgebra.equiv_symm_comp

Modification history

2026-05-21 08:11

Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean

refactor(Algebra): replace `SemilinearEquivClass.semilinearEquiv` by structure-specific coercions (#37944) …

Modified IsSymmetricAlgebra.equiv_symm_comp View on Github →

2025-11-26 08:20

Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean

feat(LinearAlgebra/SymmetricAlgebra): IsSymmetricAlgebra (#27308) …

Added IsSymmetricAlgebra.equiv_symm_comp View on Github →