mathlib3
246f6f79 - feat(algebra/group_with_zero): add lemmas about `f * pi.single i x` (#6418)

Commit

2 years ago

feat(algebra/group_with_zero): add lemmas about `f * pi.single i x` (#6418) Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Author

urkud

Parents