Commit 2023-12-19 12:00 7d208e64

View on Github →

feat: Preimage of pointwise multiplication (#8956) From PFR

Estimated changes

Modified Mathlib/Data/Finset/Pointwise.lean

added theorem Set.card_div_le

added theorem Set.card_inv

added theorem Set.card_mul_le

added theorem Set.card_smul_set

Modified Mathlib/Data/Nat/Totient.lean

Modified Mathlib/Data/Set/Finite.lean

modified theorem Set.Finite.of_preimage

modified theorem Set.Finite.preimage

added theorem Set.Infinite.preimage'

added theorem Set.finite_image2

modified theorem Set.finite_of_finite_preimage

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

added theorem Set.div_subset_range

added theorem Set.mul_subset_range

added theorem Set.preimage_div

added theorem Set.preimage_mul

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

added theorem Set.finite_mul

Modified Mathlib/NumberTheory/MaricaSchoenheim.lean

Modified Mathlib/SetTheory/Cardinal/Finite.lean

added theorem Nat.card_eq_card_finite_toFinset

added theorem Nat.card_eq_card_toFinset

added theorem Nat.card_eq_finsetCard

added theorem Nat.card_image_equiv

added theorem Nat.card_image_le

added theorem Nat.card_image_of_injOn

added theorem Nat.card_image_of_injective

modified theorem Nat.card_mono

added theorem Nat.card_preimage_of_injOn

added theorem Nat.card_preimage_of_injective

added theorem Set.card_prod_singleton

added theorem Set.card_singleton_prod