Mathlib v3 is deprecated. Go to Mathlib v4

Theorem divp_left_inj

Modification history

2022-01-05 23:45
src/algebra/group/units.lean
chore(*): notation for `units` (#11236)
Modified divp_left_injView on Github →
2020-05-18 13:38
src/algebra/group/units.lean
refactor(algebra): merge init_.algebra into algebra (#2707) …
Modified divp_left_injView on Github →
2020-05-12 15:37
src/algebra/group/units.lean
chore(*): unify use of left and right for injectivity lemmas (#2655) …
Added divp_left_injView on Github →