Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_localized_module.lift_comp

Modification history

2022-09-30 23:37

src/algebra/module/localized_module.lean

feat(algebra/module/localized_module): universal property of localized module (#15559) …

Added is_localized_module.lift_comp View on Github →