mathlib
5decc005 - More `cast` lemmas that don't need `@[simp]` anymore

Commit

3 years ago

More `cast` lemmas that don't need `@[simp]` anymore

Author

Vierkantor

Vierkantor

Committer

Vierkantor

Vierkantor

Parents

Loading