Theorem Submodule.quotientRel_def

Modification history

2024-10-29 16:55
Mathlib/LinearAlgebra/Quotient/Basic.lean
chore(LinearAlgebra): split `Quotient.lean` into `Defs` and `Basic` (#18384) …
Modified Submodule.quotientRel_defView on Github →
2024-10-09 16:54
Mathlib/LinearAlgebra/Quotient.lean
chore: remove some `Setoid.r` (#16258)
Added Submodule.quotientRel_defView on Github →