Commit 2025-08-03 21:39 ad1449f5

View on Github →

feat: a finite union of proper submodules is a proper subset (#27598) (provided the coefficients are a sufficiently large field).

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/Submodule/Union.lean

added theorem Module.Dual.exists_forall_mem_ne_zero_of_forall_exists

added theorem Module.Dual.exists_forall_ne_zero_of_forall_exists

added theorem Submodule.exists_forall_notMem_of_forall_ne_top

added theorem Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.natCast_lt_succ

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Set/Card.lean

added theorem Function.Injective.encard_range

added theorem Set.encard_ne_add_one

added theorem Set.exists_ne_map_eq_of_encard_lt_of_maps_to