Theorem Submodule.Quotient.mk_out

Modification history

2025-07-02 08:48
Mathlib/LinearAlgebra/Quotient/Defs.lean
feat(RingTheory): lemmas about `TensorProduct` and `IsBaseChange` (#26297) …
Added Submodule.Quotient.mk_outView on Github →