mathlib3
58b1429a - chore(algebra/group/pi): `pow_apply` can be `rfl` (#11249)

Commit

4 years ago

chore(algebra/group/pi): `pow_apply` can be `rfl` (#11249)

Author

urkud

urkud

Parents

Loading