Commit 2026-09-07 15:38 059a625d

View on Github →

feat(Algebra/Group/Pointwise): sdiv lemmas (#43541) Ported over from #8608 and extended slightly

Estimated changes

added theorem Finset.Nonempty.sdiv
deleted theorem Finset.Nonempty.vsub
added theorem Finset.coe_sdiv
deleted theorem Finset.coe_vsub
added theorem Finset.empty_sdiv
deleted theorem Finset.empty_vsub
deleted theorem Finset.image_vsub_product
deleted theorem Finset.inter_vsub_subset
added theorem Finset.mem_sdiv
deleted theorem Finset.mem_vsub
added theorem Finset.sdiv_card_le
added theorem Finset.sdiv_def
added theorem Finset.sdiv_empty
added theorem Finset.sdiv_eq_empty
added theorem Finset.sdiv_mem_sdiv
added theorem Finset.sdiv_nonempty
added theorem Finset.sdiv_singleton
added theorem Finset.sdiv_subset_iff
added theorem Finset.sdiv_union
added theorem Finset.singleton_sdiv
deleted theorem Finset.singleton_vsub
added theorem Finset.subset_sdiv
deleted theorem Finset.subset_vsub
added theorem Finset.union_sdiv
deleted theorem Finset.union_vsub
deleted theorem Finset.vsub_card_le
deleted theorem Finset.vsub_def
deleted theorem Finset.vsub_empty
deleted theorem Finset.vsub_eq_empty
deleted theorem Finset.vsub_inter_subset
deleted theorem Finset.vsub_mem_vsub
deleted theorem Finset.vsub_nonempty
deleted theorem Finset.vsub_singleton
deleted theorem Finset.vsub_subset_iff
deleted theorem Finset.vsub_subset_vsub
deleted theorem Finset.vsub_union
deleted theorem Set.Finite.toFinset_vsub
added theorem Set.toFinset_sdiv
deleted theorem Set.toFinset_vsub
added theorem Set.Finite.sdiv
deleted theorem Set.Finite.vsub
added theorem Set.iInter_sdiv_subset
deleted theorem Set.iInter_vsub_subset
deleted theorem Set.iInter₂_vsub_subset
added theorem Set.iUnion_sdiv
deleted theorem Set.iUnion_vsub
added theorem Set.iUnion₂_sdiv
deleted theorem Set.iUnion₂_vsub
added theorem Set.sInter_sdiv_subset
deleted theorem Set.sInter_vsub_subset
added theorem Set.sUnion_sdiv
deleted theorem Set.sUnion_vsub
added theorem Set.sdiv_iInter_subset
added theorem Set.sdiv_iUnion
added theorem Set.sdiv_iUnion₂
added theorem Set.sdiv_sInter_subset
added theorem Set.sdiv_sUnion
deleted theorem Set.vsub_iInter_subset
deleted theorem Set.vsub_iInter₂_subset
deleted theorem Set.vsub_iUnion
deleted theorem Set.vsub_iUnion₂
deleted theorem Set.vsub_sInter_subset
deleted theorem Set.vsub_sUnion
deleted theorem Filter.NeBot.of_vsub_left
added theorem Filter.bot_sdiv
deleted theorem Filter.bot_vsub
added theorem Filter.le_sdiv_iff
deleted theorem Filter.le_vsub_iff
added theorem Filter.map₂_sdiv
deleted theorem Filter.map₂_vsub
added theorem Filter.mem_sdiv
deleted theorem Filter.mem_vsub
added theorem Filter.pure_sdiv
added theorem Filter.pure_sdiv_pure
deleted theorem Filter.pure_vsub
deleted theorem Filter.pure_vsub_pure
added theorem Filter.sdiv.instNeBot
added theorem Filter.sdiv_bot
added theorem Filter.sdiv_eq_bot_iff
added theorem Filter.sdiv_le_sdiv
added theorem Filter.sdiv_mem_sdiv
added theorem Filter.sdiv_neBot_iff
added theorem Filter.sdiv_pure
deleted theorem Filter.vsub.instNeBot
deleted theorem Filter.vsub_bot
deleted theorem Filter.vsub_eq_bot_iff
deleted theorem Filter.vsub_le_vsub
deleted theorem Filter.vsub_le_vsub_left
deleted theorem Filter.vsub_le_vsub_right
deleted theorem Filter.vsub_mem_vsub
deleted theorem Filter.vsub_neBot_iff
deleted theorem Filter.vsub_pure