Commit 2022-12-17 09:24 c2337ec8
View on Github →chore(number_theory/divisors): golf (#17954)
- Upgrade
nat.swap_mem_divisors_antidiagonalto asimpifflemma. - Use
(equiv.prod_comm _ _).to_embeddinginstead of⟨prod.swap, _⟩. - Golf.
chore(number_theory/divisors): golf (#17954)
nat.swap_mem_divisors_antidiagonal to a simp iff lemma.(equiv.prod_comm _ _).to_embedding instead of ⟨prod.swap, _⟩.