Commit 2023-01-29 03:26 ba2a530c

View on Github →

feat: port Data.Set.Pointwise.Finite (#1844)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Pointwise/Basic.lean

Created Mathlib/Data/Set/Pointwise/Finite.lean

added theorem Group.card_pow_eq_card_pow_card_univ

added theorem Set.Finite.inv

added theorem Set.Finite.mul

added theorem Set.Finite.smul

added theorem Set.Finite.smul_set

added theorem Set.Finite.vsub

added def Set.fintypeMul