mathlib3
48dec300 - chore(algebra/module/basic): use `simp` instead of `norm_num` (#15670)

Commit

3 years ago

chore(algebra/module/basic): use `simp` instead of `norm_num` (#15670)

Author

urkud

urkud

Parents

Loading