Theorem Submodule.Quotient.mk_zero

Modification history

2024-10-29 16:55

Mathlib/LinearAlgebra/Quotient/Basic.lean

chore(LinearAlgebra): split `Quotient.lean` into `Defs` and `Basic` (#18384) …

Modified Submodule.Quotient.mk_zero View on Github →

2023-02-18 20:01

Mathlib/LinearAlgebra/Quotient.lean

feat: port LinearAlgebra.Quotient (#2286) …

Added Submodule.Quotient.mk_zero View on Github →