Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-05 18:03 394d7213

View on Github →

feat(algebra/module): add quotient module

Estimated changes

Modified algebra/module.lean

added theorem is_submodule.is_linear_map_quotient_lift

added theorem is_submodule.is_linear_map_quotient_mk

added theorem is_submodule.quotient.injective_lift

added def is_submodule.quotient.lift

added def is_submodule.quotient

added def is_submodule.quotient_rel