Def Basis.smulTower

Modification history

2024-12-16 14:33

Mathlib/RingTheory/AlgebraTower.lean

feat(LinearAlgebra): general transitivity of norm (#19978) …

Modified Basis.smulTower View on Github →

2024-07-24 14:53

Mathlib/RingTheory/AlgebraTower.lean

fix: shorten lines with 101 characters (#15104) …

Added Basis.smulTower View on Github →