mathlib3
94cbfad7 - chore(algebra/*): move some lemmas about is_unit from associated.lean (#12526)

Commit

3 years ago

chore(algebra/*): move some lemmas about is_unit from associated.lean (#12526) There doesn't seem to be any reason for them to live there.

Author

Ruben-VandeVelde

Parents