mathlib3
c2337ec8
- chore(number_theory/divisors): golf (#17954)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(number_theory/divisors): golf (#17954) * Upgrade `nat.swap_mem_divisors_antidiagonal` to a `simp` `iff` lemma. * Use `(equiv.prod_comm _ _).to_embedding` instead of `⟨prod.swap, _⟩`. * Golf.
Author
urkud
Parents
706d88f2
Loading