mathlib
4dc4dc8b - chore(topology/algebra/module/basic): cleanup variables and coercions (#12542)

Commit
3 years ago
chore(topology/algebra/module/basic): cleanup variables and coercions (#12542) Having the "simple" variables in the lemmas statements rather than globally makes it easier to move lemmas around in future. This also mean lemmas like `coe_comp` can have their arguments in a better order, as it's easier to customize the argument order at the declaration. This also replaces a lot of `(_ : M₁ → M₂)`s with `⇑_` for brevity in lemma statements. No lemmas statements (other than argument reorders) or proofs have changed.
Author
Parents
Loading