Theorem LinearEquiv.isScalarTower

Modification history

2025-07-14 05:43

Mathlib/Algebra/Equiv/TransferInstance.lean

chore(Algebra/Equiv/TransferInstance): split according to algebraic structures (#26732) …

Modified LinearEquiv.isScalarTower View on Github →

2024-12-20 22:32

Mathlib/Algebra/Equiv/TransferInstance.lean

feat(RingTheory/Flat): generalize `flat_of_isLocalized_span` (#19788) …

Added LinearEquiv.isScalarTower View on Github →