Theorem LinearMap.baseChangeHom_injective

Modification history

2026-04-29 11:39

Mathlib/RingTheory/Flat/Basic.lean

feat: drop IsAlgClosed hypothesis from isNilpotent_derivedSeries_of_traceForm_eq_zero_algClosed (#38542) …

Added LinearMap.baseChangeHom_injective View on Github →