Theorem PiTensorProduct.submodule_span_eq_top

Modification history

2026-06-18 10:07
Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean
feat(LinearAlgebra): generators of pi tensor products (#26464) …
Added PiTensorProduct.submodule_span_eq_topView on Github →