Theorem Pi.dim_spanSubset

Modification history

2026-10-10 13:11
Mathlib/LinearAlgebra/Dimension/Constructions.lean
feat(LinearAlgebra): make two `Nontrivial` theorems low priority instances (#44558) …
Modified Pi.dim_spanSubsetView on Github →
2026-02-24 20:40
Mathlib/LinearAlgebra/Dimension/Constructions.lean
feat(LinearAlgebra/QuadraticForm): radical of a quadratic form (#34493) …
Added Pi.dim_spanSubsetView on Github →