Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_dvd_of_is_unit_left

Modification history

2020-08-11 09:57
src/algebra/associated.lean
refactor(algebra/divisibility, associated): generalize instances in divisibility, associated (#3714) …
Deleted mul_dvd_of_is_unit_leftView on Github →
2018-11-05 10:47
ring_theory/associated.lean
feat(linear_algebra,ring_theory): refactoring modules (#456) …
Added mul_dvd_of_is_unit_leftView on Github →