Commit 2023-12-17 15:16 f4794c25

View on Github →

chore(Ideal/Operations): remove extraneous nonempty conditions (#9115) Also generalizes Ideal.subset_union to Subgroup.

Estimated changes

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

added theorem SubgroupClass.subset_union

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

modified theorem Ideal.IsPrime.inf_le'

modified theorem Ideal.IsPrime.mul_le

modified theorem Ideal.IsPrime.multiset_prod_le

modified theorem Ideal.IsPrime.prod_le