mathlib
5ba8491c - Remove the `@[simp]` attribute from `coe_fn_coe_base`

Commit

5 years ago

Remove the `@[simp]` attribute from `coe_fn_coe_base`

Author

Vierkantor

Vierkantor

Committer

Vierkantor

Vierkantor

Parents

Loading