Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_submodule.neg_val

Modification history

2017-12-08 17:29
algebra/module.lean
refactor(algebra/module): split of type constructions and move quotient, subtype and linear_map to their own theories in algebra/linear_algebra
Deleted is_submodule.neg_valView on Github →
2017-12-05 15:23
algebra/module.lean
fix(theories/number_theory/pell,*): fix broken proofs, less simp AC
Modified is_submodule.neg_valView on Github →
2017-12-05 14:35
algebra/module.lean
refactor(algebra/module): clean up is_submodule projections
Modified is_submodule.neg_valView on Github →
2017-12-05 14:15
algebra/module.lean
refactor(algebra/module): rename submodule -> is_submodule, smul_left_distrib -> smul_add, smul_right_distrib -> add_smul, smul_sub_left_distrib -> smul_sub, sub_smul_right_distrib -> sub_smul
Added is_submodule.neg_valView on Github →