Def Finset.imageMulHom

Modification history

2024-08-02 06:24

Mathlib/Data/Finset/Pointwise.lean

chore: backports for leanprover/lean4#4814 (part 12) (#15396) …

Modified Finset.imageMulHom View on Github →

2023-02-05 11:33

Mathlib/Data/Finset/Pointwise.lean

fix: use `to_additive (attr := _)` here and there (#2073)

Modified Finset.imageMulHom View on Github →

2023-02-01 10:16

Mathlib/Data/Finset/Pointwise.lean

feat: Port/Data.Finset.Pointwise (#1911) …

Added Finset.imageMulHom View on Github →