Commit 2020-11-25 06:48 0324935c
View on Github →chore(data/equiv/basic): Add trivial simp lemma (#5100)
With this in place, ⇑1 ∘ f simplifies to ⇑f
chore(data/equiv/basic): Add trivial simp lemma (#5100)
With this in place, ⇑1 ∘ f simplifies to ⇑f