Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-11 14:09 ee7ede9e

View on Github →

feat(algebra/linear_algebra): proof first and second isomorphism laws

Estimated changes

Modified algebra/linear_algebra/linear_map_module.lean

added theorem classical.some_spec2

added theorem linear_map.is_submodule.add_left_iff

added theorem linear_map.is_submodule.neg_iff

added def linear_map.quot_ker_equiv_im

added def linear_map.union_quotient_equiv_quotient_inter

Modified algebra/linear_algebra/quotient_module.lean

added theorem is_submodule.quotient.lift_mk

added theorem is_submodule.quotient_rel_eq

Modified algebra/linear_algebra/subtype_module.lean

modified theorem is_linear_map_subtype_mk

modified theorem sub_val