Commit 2023-12-27 20:59 7b59a5fa

View on Github →

feat: (a • s)⁻¹ = s⁻¹ • a⁻¹ (#9199) and other simple pointwise lemmas for Set and Finset. Also add supporting Fintype.piFinset lemmas and fix the names of two lemmas. From LeanAPAP and LeanCamCombi

Estimated changes

added theorem Finset.pi_nonempty
modified theorem Finset.Nonempty.smul_zero
modified theorem Finset.Nonempty.zero_smul
modified theorem Finset.card_inv
added theorem Finset.coe_eq_one
modified theorem Finset.coe_inv
deleted theorem Finset.image_div_prod
added theorem Finset.image_op_inv
added theorem Finset.inv_univ
added theorem Finset.mem_inv'
modified theorem Finset.preimage_inv
added theorem Finset.prod_inv_index
added theorem Finset.prod_neg_index
modified theorem Finset.smul_finset_univ₀
added theorem Finset.smul_univ₀'
modified theorem Finset.smul_zero_subset
added theorem Finset.sum_inv_index
added theorem Finset.univ_div_univ
modified theorem Finset.zero_mem_smul_finset
modified theorem Finset.zero_mem_smul_iff
modified theorem Finset.zero_smul_finset
modified theorem Finset.zero_smul_subset
added theorem Fintype.piFinset_div
added theorem Fintype.piFinset_inv
added theorem Fintype.piFinset_mul
added theorem Fintype.piFinset_smul
added theorem Fintype.piFinset_image
added theorem Set.univ_div_univ
modified theorem Set.zero_smul_set