Union

📁 Source: Mathlib/Algebra/Module/Submodule/Union.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_forall_mem_ne_zero_of_forall_exists, exists_forall_ne_zero_of_forall_exists, exists_dual_forall_apply_ne_zero, exists_forall_notMem_of_forall_ne_top, iUnion_ssubset_of_forall_ne_top_of_card_lt	5
Total	5

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_dual_forall_apply_ne_zero 📖	mathematical	—	Dual DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	—	Dual.exists_forall_ne_zero_of_forall_exists smulCommClass_self Projective.of_free Free.of_divisionRing

Module.Dual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_forall_mem_ne_zero_of_forall_exists 📖	mathematical	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike	—	exists_forall_ne_zero_of_forall_exists
exists_forall_ne_zero_of_forall_exists 📖	—	—	—	—	Submodule.exists_forall_notMem_of_forall_ne_top

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_forall_notMem_of_forall_ne_top 📖	mathematical	—	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid SetLike.instMembership setLike	—	Set.iUnion_congr_Prop Set.iUnion_true iUnion_ssubset_of_forall_ne_top_of_card_lt ENat.card_eq_top_of_infinite
iUnion_ssubset_of_forall_ne_top_of_card_lt 📖	mathematical	ENat instLTENat ENat.instNatCast Finset.card ENat.card	Set Set.instHasSSubset Set.iUnion Finset SetLike.instMembership Finset.instSetLike SetLike.coe Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid setLike Set.univ	—	Finset.induction_on Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty Zero.instNonempty Finset.eq_empty_or_nonempty Finset.instLawfulSingleton Set.iUnion_iUnion_eq_left Finset.card_insert_of_notMem Nat.cast_add Nat.cast_one Mathlib.Tactic.Contrapose.contrapose₄ Set.iUnion_iUnion_eq_or_left eq_or_ne AddSubmonoidClass.toZeroMemClass addSubmonoidClass Mathlib.Tactic.Contrapose.contrapose₂ ext Set.disjoint_iff smul_mem_iff IsScalarTower.left add_mem_iff_right Disjoint.subset_right_of_subset_union Set.subset_univ lt_of_add_lt_add_right contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid lt_of_lt_of_le smul_left_injective IsDomain.toIsCancelMulZero instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors AddLeftCancelSemigroup.toIsLeftCancelAdd Set.ext Function.Injective.encard_image Set.encard_ne_add_one le_refl Set.exists_ne_map_eq_of_encard_lt_of_maps_to Set.encard_coe_eq_coe_finsetCard Set.encard_univ Set.mem_univ Subtype.coe_ne_coe Set.iUnion_true Set.mem_iUnion Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval₃ add_zero Mathlib.Tactic.Module.NF.sub_eq_eval₂ Mathlib.Tactic.Module.NF.zero_sub_eq_eval Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Module.NF.eq_const_cons Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add sub_mem addSubgroupClass sub_ne_zero add_sub_cancel_right smul_mem Set.union_eq_right lt_trans ENat.natCast_lt_succ

---

← Back to Index