Theorem LinearMap.BilinForm.baseChange_zero

Modification history

2026-04-29 11:39
Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean
feat: drop IsAlgClosed hypothesis from isNilpotent_derivedSeries_of_traceForm_eq_zero_algClosed (#38542) …
Added LinearMap.BilinForm.baseChange_zeroView on Github →