Commit 2024-08-03 13:28 6695aaa6

View on Github →

chore: backports for leanprover/lean4#4814 (part 14) (#15406)

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

modified theorem AddMonoidAlgebra.apply_eq_zero_of_not_le_supDegree

Modified Mathlib/Algebra/Star/Subalgebra.lean

Modified Mathlib/LinearAlgebra/Dimension/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

modified theorem LinearMap.toMatrix_prodMap

modified theorem Matrix.vecMul_stdBasis

Modified Mathlib/Topology/AlexandrovDiscrete.lean

modified theorem Inducing.alexandrovDiscrete

Modified Mathlib/Topology/Compactness/SigmaCompact.lean