mathlib

73b41b2c - chore(data/prod): rename `injective_prod` to `injective.prod` (#2058)

chore(data/prod): rename `injective_prod` to `injective.prod` (#2058) This way we can use dot notation Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>