mathlib
938eeeb4 - feat(algebra/group/with_one): add a recursor and a `no_zero_divisors` instance (#14434)

Commit
3 years ago
feat(algebra/group/with_one): add a recursor and a `no_zero_divisors` instance (#14434)
Author
Parents
Loading