| Name | Category | Theorems |
|---|
closure 📖 | CompOp | 144 mathmath: AddCommute.exists_addOrderOf_eq_lcm, Ideal.Filtration.submodule_closure_single, Submonoid.subsemiringClosure_toAddSubmonoid, add_subset_closure, Subsemiring.closure_addSubmonoid_closure, closure_sdiff_eq_closure, sup_eq_closure, IsLinearSet.closure_finset, multiples_eq_closure, mem_closure_finset, AddMonoid.closure_finite_fg, AddMonoid.fg_iff, frobeniusNumber_iff, closure_addIrreducible, closure_nsmul, IsSemilinearSet.closure_finset, Set.IsPWO.addSubmonoid_closure, Nat.exists_mem_closure_of_ge, closure_sdiff_singleton_zero, mem_closure_range_iff, Submonoid.subsemiringClosure_coe, Submodule.closure_le_toAddSubmonoid_span, StarOrderedRing.lt_iff, isLinearSet_iff, smul_mem_closure_star_mul, closure_le_centralizer_centralizer, nsmul_vadd_mem_closure_vadd, closure_prod, closure_pi, closure_image_isAddIndecomposable_baseOf, StarOrderedRing.pos_iff, closure_univ, Nat.addSubmonoidClosure_one, Submonoid.toAddSubmonoid_closure, RootPairing.coroot_mem_or_neg_mem_closure_of_root, toNatSubmodule_closure, NonUnitalSubsemiring.closure_addSubmonoid_closure, IsLinearSet.closure_of_finite, closure_union, closure_isSquare, mem_closure_iff_exists_finset_subset, AddMonoidHom.mclosure_preimage_le, subset_closure, AddMonoidHom.map_mclosure, closure_singleton_eq, closure_zero_prod, toSubmonoid_closure, AddMonoid.closure_finset_fg, HahnSeries.SummableFamily.support_pow_subset_closure, exists_minimal_closure_eq_top, dense_addSubmonoidClosure_iff_addSubgroupClosure, IsSemilinearSet.closure_of_finite, Subsemigroup.nonUnitalSubsemiringClosure_coe, AddSubgroup.closure_toAddSubmonoid, fg_iff, Rat.addSubmonoid_closure_range_pow, closure_nsmul_le, isProperLinearSet_iff, closure_addSubmonoidClosure_eq_closure_addSubgroupClosure, closure_insert_zero, IsLinearSet.closure, mem_closure_of_mem, unop_closure, smul_closure, MulMemClass.mul_right_mem_add_closure, pow_eq_closure_pow_set, Submodule.span_eq_closure, Submodule.closure_subset_span, closure_eq, Rat.addSubmonoid_closure_range_mul_self, topologicalClosure_addSubgroupClosure_toAddSubmonoid, DFinsupp.add_closure_iUnion_range_single, closure_closure_coe_preimage, NNRat.addSubmonoid_closure_range_pow, mem_closure_image_pos_iff, AddSubgroup.closure_toAddSubmonoid_of_finite, FreeAddMonoid.closure_range_of, instIsAddCommutative_closure, FreeAddMonoid.mrange_lift, MulMemClass.mul_mem_add_closure, AddMonoidHom.mclosure_range, one_eq_closure, MulMemClass.mul_left_mem_add_closure, closure_add_le, AddSubgroup.closure_toAddSubmonoid_of_isOfFinAddOrder, one_eq_closure_one_set, Submodule.span_nat_eq_addSubmonoidClosure, Int.addSubmonoid_closure_range_pow, IsAddIndecomposable.apply_ne_zero_iff_mem_closure, mem_closure, closure_neg, closure_prod_zero, closure_pow, StarOrderedRing.le_iff, Finsupp.add_closure_setOf_eq_single, mem_closure_iff_of_fintype, sup_eq_closure_add, RootPairing.Base.root_mem_or_neg_mem, closure_eq_image_sum, AddMonoid.Coprod.mclosure_range_inl_union_inr, RootPairing.eq_baseOf_iff, Subsemiring.coe_closure_eq, closure_singleton_zero, StarOrderedRing.nonneg_iff, closure_le, addIrreducible_mem_addSubmonoidClosure_subset, mem_closure_range_iff_of_fintype, FG.exists_minimal_closure_eq, PresentedAddMonoid.closure_range_of, closure_eq_of_le, RootPairing.Base.coroot_mem_or_neg_mem, op_closure, AddMonoidHom.eqOn_closureM, Polynomial.addSubmonoid_closure_setOf_eq_monomial, mem_closure_pair, AddSubgroup.le_closure_toAddSubmonoid, Submodule.span_closure, closure_iUnion, Submonoid.toAddSubmonoid'_closure, mem_closure_neg, LieAlgebra.Basis.root_mem_or_mem_neg, HomogeneousIdeal.irrelevant_eq_closure, NNRat.addSubmonoid_closure_range_mul_self, IsSemilinearSet.closure, Submonoid.subsemiringClosure_mem, Int.addSubmonoid_closure_range_mul_self, mem_closure_singleton, mem_closure_finset', NonUnitalSubsemiring.mem_closure_iff, Nat.one_mem_closure_iff, closure_eq_mrange, isAddCommutative_closure, Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid, NonUnitalSubsemiring.coe_closure_eq, closure_empty, AddMonoidAlgebra.mem_closure_of_mem_span_closure, IsAddIndecomposable.mem_or_neg_mem_closure_baseOf, Subsemiring.mem_closure_iff, toSubmonoid'_closure, closure_singleton_le_iff_mem, closure_mul_closure, closure_mono, iSup_eq_closure, mul_eq_closure_mul_set
|
gi 📖 | CompOp | — |
instCompleteLattice 📖 | CompOp | 88 mathmath: smul_iSup, sup_eq_closure, op_sup, AddCommMonoid.primaryComponent.disjoint, iSup_map_single, fixedPoints_addSubmonoid_iSup, sup_mul, smul_sup, AddMonoid.Coprod.mrange_lift, closure_union, neg_sup, FG.iSup, mul_iSup, disjoint_def', iSup_map_single_le, sup_eq_range, mem_bsupr_iff_exists_dfinsupp, unop_iSup, Submodule.toAddSubmonoid_sSup, mem_iSup, AddSubgroup.ofAddUnits_sSup, mul_sup, AddMonoid.Coprod.codisjoint_mrange_inl_mrange_inr, exists_mem_sup, fixedPoints_addSubmonoid_sup, iSup_eq_mrange_dfinsuppSumAddHom, AddSubgroup.ofAddUnits_inf, coe_iSup_of_directed, coe_sSup_of_directedOn, add_mem_sup, unop_sSup, AddMonoidHom.noncommPiCoprod_mrange, SaturatedAddSubmonoid.sSup_def, mrange_inl_sup_mrange_inr, bsupr_eq_mrange_dfinsuppSumAddHom, FG.biSup, coe_sup, AddSubgroup.ofAddUnits_iSup₂, op_sSup, op_iSup, mem_iSup_of_directed, closure_add_le, DirectSum.IsInternal.addSubmonoid_iSup_eq_top, SaturatedAddSubmonoid.sup_def, saturation_iSup, sup_eq_closure_add, AddMonoid.Coprod.mrange_inl_sup_mrange_inr, FG.biSup_finset, saturation_sSup, codisjoint_map, map_iSup, mem_sup, map_sup_comap_of_surjective, mem_iSup_iff_exists_dfinsupp', SaturatedAddSubmonoid.iSup_def, AddSubgroup.ofAddUnits_sup_addUnits, AddSubgroup.toAddSubmonoid_zmultiples, mem_iSup_iff_exists_dfinsupp, HomogeneousIdeal.irrelevant_eq_iSup, AddMonoid.Coprod.mrange_eq, disjoint_def, saturation_sup, closure_iUnion, mem_sSup_of_mem, Submodule.sup_toAddSubmonoid, map_sup, addSubmonoid_smul_sup, mem_iSup_of_mem, map_iSup_comap_of_surjective, FG.finset_sup, neg_iSup, comap_iSup_map_of_injective, mem_biSup_of_directedOn, prod_bot_sup_bot_prod, iSup_mul, AddSubgroup.ofAddUnits_iSup, FG.sup, unop_sup, Submodule.iSup_toAddSubmonoid, mem_sup_left, DirectSum.IsInternal.addSubmonoid_iSupIndep, mem_sSup_of_directedOn, comap_sup_map_of_injective, iSupIndep_of_dfinsuppSumAddHom_injective, mem_sup_right, iSup_eq_closure, disjoint_map, mem_iSup_prop
|
instInfSet 📖 | CompOp | 21 mathmath: neg_iInf, addUnits_iInf₂, addUnits_sInf, comap_iInf, unop_iInf, addUnits_iInf, mem_sInf, coe_iInf, Subsemiring.sInf_toAddSubmonoid, AddSaturated.sInf, coe_sInf, unop_sInf, mem_iInf, AddSaturated.iInf, NonUnitalSubsemiring.sInf_toAddSubmonoid, op_sInf, map_iInf_comap_of_surjective, comap_iInf_map_of_injective, map_iInf, op_iInf, fixingAddSubmonoid_iUnion
|
| Name | Category | Theorems |
|---|
closure 📖 | CompOp | 100 mathmath: mem_closure_iff_of_fintype, MonoidHom.eqOn_closureM, closure_pow, IsMulIndecomposable.mem_or_inv_mem_closure_baseOf, closure_singleton_le_iff_mem, mem_closure, RootPairing.weylGroup_toSubmonoid, closure_pow_le, mem_closure_singleton_self, closure_pi, Subgroup.closure_toSubmonoid, Equiv.Perm.mclosure_swap_castSucc_succ, Set.IsPWO.submonoid_closure, iSup_eq_closure, Commute.exists_orderOf_eq_lcm, toAddSubmonoid_closure, sup_eq_closure_mul, Monoid.CoprodI.mclosure_iUnion_range_of, PresentedMonoid.closure_range_of, closure_eq_one_union, closure_singleton_eq, closure_univ, exists_minimal_closure_eq_top, FreeMonoid.closure_range_of, AddSubmonoid.toSubmonoid_closure, Subring.mem_closure_iff, closure_eq_of_le, powers_eq_closure, mem_closure_singleton, instIsMulCommutative_closure, closure_mono, mul_subset_closure, Algebra.adjoin_toSubmodule_le, closure_prod_one, closure_eq, isMulCommutative_closure, topologicalClosure_subgroupClosure_toSubmonoid, Subgroup.le_closure_toSubmonoid, Monoid.closure_finset_fg, divisor_closure_eq_closure, closure_le_centralizer_centralizer, Monoid.fg_iff, MonoidHom.mclosure_preimage_le, MonoidAlgebra.mem_closure_of_mem_span_closure, FreeMonoid.mrange_lift, closure_mul_le, dense_submonoidClosure_iff_subgroupClosure, closure_submonoidClosure_eq_closure_subgroupClosure, Algebra.adjoin_eq_span, fg_iff, Subsemiring.coe_closure_eq, MonoidWithZeroHom.valueMonoid_eq_closure, closure_empty, closure_prod, closure_sdiff_singleton_one, mem_closure_finset, closure_image_isMulIndecomposable_baseOf, op_closure, mem_closure_range_iff, smul_closure, closure_insert_one, closure_sdiff_eq_closure, mem_closure_range_iff_of_fintype, closure_union, mem_closure_inv, Monoid.Coprod.mclosure_range_inl_union_inr, StarAlgebra.adjoin_eq_span, toAddSubmonoid'_closure, Subsemiring.closure_submonoid_closure, mem_closure_finset', Monoid.closure_finite_fg, irreducible_mem_submonoidClosure_subset, closure_singleton_one, MonoidHom.map_mclosure, closure_iUnion, mem_closure_of_mem, closure_image_one_lt_and_isMulIndecomposable, CoxeterSystem.submonoid_closure_range_simple, pow_smul_mem_closure_smul, closure_closure_coe_preimage, Equiv.Perm.mclosure_isSwap, closure_inv, MonoidHom.mclosure_range, unop_closure, closure_irreducible, subset_closure, FG.exists_minimal_closure_eq, IsMulIndecomposable.apply_ne_one_iff_mem_closure, Subgroup.closure_toSubmonoid_of_isOfFinOrder, Subsemiring.mem_closure_iff, sup_eq_closure, closure_le, mem_closure_pair, mem_closure_iff_exists_finset_subset, mem_closure_image_one_lt_iff, Subgroup.closure_toSubmonoid_of_finite, AddSubmonoid.toSubmonoid'_closure, closure_eq_mrange, closure_eq_image_prod, closure_one_prod
|
gi 📖 | CompOp | — |
instCompleteLattice 📖 | CompOp | 72 mathmath: saturation_iSup, SaturatedSubmonoid.iSup_def, comap_sup_map_of_injective, unop_iSup, coe_iSup_of_directed, map_sup_comap_of_surjective, mem_sup, iSup_eq_closure, coe_sSup_of_directedOn, mrange_inl_sup_mrange_inr, prod_bot_sup_bot_prod, mem_iSup, Monoid.CoprodI.mrange_eq_iSup, iSup_map_mulSingle_le, Monoid.Coprod.mrange_eq, sup_eq_closure_mul, mem_sup_left, mem_sSup_of_directedOn, op_sSup, fixedPoints_submonoid_sup, smul_sup, FG.finset_sup, map_iSup, iSup_map_mulSingle, map_sup, op_iSup, inv_sup, Subgroup.toSubmonoid_zpowers, mem_iSup_prop, Subgroup.ofUnits_inf, Monoid.Coprod.mrange_lift, map_iSup_comap_of_surjective, comap_iSup_map_of_injective, op_sup, CommMonoid.primaryComponent.disjoint, inv_iSup, fixedPoints_submonoid_iSup, mem_iSup_of_directed, unop_sup, MonoidHom.noncommPiCoprod_mrange, FG.iSup, closure_mul_le, mul_mem_sup, coe_sup, Monoid.CoprodI.iSup_mrange_of, unop_sSup, SaturatedSubmonoid.sup_def, mem_sup_right, FG.sup, disjoint_map, mem_biSup_of_directedOn, codisjoint_map, Subgroup.ofUnits_iSup₂, closure_union, mem_sSup_of_mem, Subgroup.ofUnits_sSup, mem_iSup_of_mem, saturation_sSup, closure_iUnion, disjoint_def', SaturatedSubmonoid.sSup_def, FG.biSup_finset, sup_eq_range, disjoint_def, Subgroup.ofUnits_iSup, Monoid.Coprod.mrange_inl_sup_mrange_inr, Monoid.Coprod.codisjoint_mrange_inl_mrange_inr, sup_eq_closure, exists_mem_sup, Subgroup.ofUnits_sup_units, FG.biSup, saturation_sup
|
instInfSet 📖 | CompOp | 24 mathmath: units_iInf, comap_iInf, op_iInf, unop_iInf, Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_iInf, comap_iInf_map_of_injective, op_sInf, MulSaturated.iInf, mem_sInf, units_sInf, MulSaturated.sInf, Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite, unop_sInf, fixingSubmonoid_iUnion, mem_iInf, units_iInf₂, map_iInf, Subring.sInf_toSubmonoid, inv_iInf, coe_iInf, Subsemiring.sInf_toSubmonoid, coe_sInf, map_iInf_comap_of_surjective, TopCat.Presheaf.submonoidPresheafOfStalk_obj
|