mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chore(ring_theory/chain_of_divisors): make some variables that can be infered implicit

Open Paul-Lez opened this issue 3 years ago • 0 comments

A few variables could be made implicit in some of the lemmas in ring_theory/chain_of_divisors. I also made a (very) minor stylistic change to a proof from one of my previous PRs in ring_theory/adjoin_root

Open in Gitpod

Paul-Lez avatar Aug 13 '22 13:08 Paul-Lez