Commit 2024-10-02 17:17 2aa61a8c

View on Github →

feat: s / t is finite (#17306) From PFR

Estimated changes

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

added theorem Set.Finite.div

deleted theorem Set.Finite.inv

added theorem Set.finite_div

added theorem Set.finite_inv

added def Set.fintypeDiv

added theorem Set.infinite_div

added theorem Set.infinite_inv

modified theorem Set.infinite_mul