Commit 2023-09-08 11:01 bce8378b
View on Github →chore: missing simps lemmas for Multiplicative defs (#7016)
This also fixes the definitions to not include any defeq abuse, which is required in order to not produce a bad simp lemma.
chore: missing simps lemmas for Multiplicative defs (#7016)
This also fixes the definitions to not include any defeq abuse, which is required in order to not produce a bad simp lemma.