Commit 2022-08-16 18:55 ea1dd3d3

View on Github →

feat(algebra/module/localized_module): add characteristic predicate for localized_module (#15507) Add characteristic predicate for localised module similar to ring localization and prove that the concrete construction satisfies the characteristic predicate.

Estimated changes

Modified src/algebra/module/localized_module.lean

added def localized_module.div_by

added theorem localized_module.div_by_mul_by

added theorem localized_module.mk_cancel

added theorem localized_module.mk_cancel_common_left

added theorem localized_module.mk_cancel_common_right

added def localized_module.mk_linear_map

added theorem localized_module.mul_by_div_by

added theorem localized_module.smul'_mk

modified theorem localized_module.zero_mk