Theorem submodule.quotient.mk_smul
Modification history
2021-12-04 01:52
src/linear_algebra/quotient.lean
feat(*): `A ⧸ B` notation for quotients in algebra (#10501) …
Modified submodule.quotient.mk_smulView on Github →2021-10-21 18:28
src/linear_algebra/quotient.lean
feat(linear_algebra/quotient): `S.restrict_scalars.quotient` is `S.quotient` (#9535) …
Modified submodule.quotient.mk_smulView on Github →