Commit 2024-12-16 14:33 2927e227

feat(LinearAlgebra): general transitivity of norm (#19978) RingTheory/AlgebraTower.lean: add a version of Basis.smulTower with the two index types swapped and associated lemmas; generalize from Ring/Group to Semiring/Monoid. LinearAlgebra/Matrix/ToLin.lean: add a lemma on the matrix representation of LinearMap.restrictScalars w.r.t. Basis.smulTower'; generalize from Ring/Group to Semiring/Monoid. RingTheory/Norm/Transitivity.lean: add the result in Silvester's paper Determinants of block matrices (with commuting, equal-sized, square blocks). The determinant can be computed by taking two determinants in a row: first over the commutative ring generated by the blocks, then over the base ring. As consequences, the determinant of LinearMap.restrictScalars can be computed by first taking a determinant and then taking a norm, and the norm satisfies transitivity in a tower of algebras. RingTheory/Norm/Basic.lean: Algebra.norm_norm is replaced by the more general version proven in Transitivity.lean. Algebra/BigOperators/Group/Finset.lean, Data/Matrix/Basic.lean, LinearAlgebra/Determinant.lean, RingTheory/Finiteness/Cardinality.lean: add one lemma in each. Data/Matrix/Block.lean: add 3 lemmas. LinearAlgebra/Matrix/Block.lean: generalize BlockTriangular from CommRing to Zero and add two lemmas. LinearAlgebra/Matrix/Determinant/Basic.lean: somehow a proof breaks and has to be fixed.