Mathlib v3 is deprecated. Go to Mathlib v4

Theorem module.End_is_unit_iff

Modification history

2022-09-30 23:37

src/algebra/algebra/basic.lean

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

Added module.End_is_unit_iff View on Github →