| Name | Category | Theorems |
|---|
comap π | CompOp | 171 mathmath: comap_lt_comap_iff_of_surjective, comap_le_comap_iff_of_le_range, LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, LinearMap.prod_eq_inf_comap, comap_zero, comap_equiv_eq_map_symm, comap_inf, map_comap_eq_of_le, LinearMap.BilinForm.ker_restrict_eq_of_codisjoint, Module.End.mem_invtSubmodule, covBy_iff_quot_is_simple, comap_neg, mem_colon', comap_op_mul, LinearMap.submoduleComap_apply_coe, comap_op_pow, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, comap_mono, comap_le_comap_smul, comap_map_eq_of_injective, biSup_comap_eq_top_of_surjective, map_comap_eq_self, comap_fst, dualAnnihilator_map_dualMap_le, le_comap_range_lTensor, biSup_comap_subtype_eq_top, Representation.Coinvariants.le_comap_ker, comap_id, map_comap_eq, map_inf_comap_of_surjective, prod_comap_inr, DFinsupp.range_mapRangeLinearMap, LinearMap.prodMap_comap_prod, goursat, comap_iInf_map_of_injective, comap_smul, LinearMap.span_preimage_le, mem_comap, DirectSum.ker_lmap, Polynomial.comap_taylorEquiv_degreeLT, Module.comap_eval_surjective, strictMono_comap_prod_map, mem_annihilator', Module.comap_jacobson_of_ker_le, comap_iSup_map_of_injective, Finsupp.supported_comap_lmapDomain, biInf_comap_proj, LinearMap.comap_leq_ker_subToSupQuotient, comap_map_eq_self, LinearEquiv.ofSubmodule'_symm_apply, comap_dualAnnihilator, LinearMap.quotientInfEquivSupQuotient_apply_mk, comap_iInf, map_inf_eq_map_inf_comap, comap_coe, CliffordAlgebra.submodule_comap_mul_reverse, LinearMap.ker_comp, isCoatom_comap_iff, KaehlerDifferential.ker_map, orderIsoMapComap_apply', comap_subtype_self, LinearMap.comap_codRestrict, comap_finsetInf, LinearMap.comap_injective, comap_sup_map_of_injective, comap_equiv_self_of_inj_of_le_apply, comap_injective_of_surjective, isCoatom_comap_or_eq_top, comap_strictMono_of_surjective, LinearMap.quotientInfEquivSupQuotient_injective, equivOpposite_apply, span_preimage_eq, LinearMap.ker_domRestrict, comap_snd, le_comap_mkQ, comap_subtype_eq_top, le_comap_map, CliffordAlgebra.ΞΉ_range_comap_involute, comap_inf_map_of_injective, comap_covBy_of_surjective, orderIsoMapComapOfBijective_symm_apply, ContinuousLinearEquiv.ofSubmodule'_apply, Module.comap_jacobson_of_bijective, comapMkQOrderEmbedding_eq, map_equiv_eq_comap_symm, comap_map_mkQ, orderIsoMapComap_symm_apply, biSup_comap_eq_top_of_range_eq_biSup, gc_map_comap, LinearEquiv.ofSubmodule'_toLinearMap, inf_comap_le_comap_add, LinearMap.range_le_iff_comap, DFinsupp.ker_mapRangeLinearMap, IsOrtho.comap_iff, comap_comp, ClosedSubmodule.toSubmodule_comap, comap_lt_of_lt_map_of_injective, Representation.le_comap_invariants, AffineMap.restrict.linear_aux, LinearMap.map_codRestrict, LinearEquiv.ofSubmodule'_apply, prod_comap_inl, map_liftQ, LieSubmodule.toSubmodule_comap, LinearMap.comap_eq_sup_ker_of_disjoint, comap_surjective_of_injective, map_iSup_comap_of_surjective, range_inclusion, LinearMap.comap_prod_prod, comap_le_comap_iff_of_surjective, smul_comap_le_comap_smul, map_iInf_comap_of_surjective, AddMonoidHom.coe_toIntLinearMap_comap, map_comap_eq_of_surjective, isCompl_comap_subtype_of_isCompl_of_le, DirectSum.range_lmap, LinearMap.le_comap_isotypicComponent, CliffordAlgebra.submodule_comap_pow_reverse, LinearMap.coe_quotientInfToSupQuotient, comap_unop_pow, map_sup_comap_of_surjective, ContinuousLinearEquiv.ofSubmodule'_symm_apply, le_comap_single_pi, LinearMap.submoduleComap_surjective_of_surjective, LinearMap.ker_restrict, CliffordAlgebra.submodule_map_reverse_eq_comap, map_comap_le, isSMulRegular_on_quot_iff_lsmul_comap_eq, CliffordAlgebra.evenOdd_comap_reverse, span_preimage_le, equivOpposite_symm_apply, SModEq.comap, map_comap_subtype, comap_unop_one, LinearMap.quotientInfEquivSupQuotient_symm_apply_left, map_le_iff_le_comap, mulMap_op, comap_smul', comap_smul'', LinearMap.range_codRestrict, CliffordAlgebra.evenOdd_comap_involute, comap_op_one, comapSubtypeEquivOfLe_apply_coe, DirectSum.isInternal_biSup_submodule_of_iSupIndep, isSMulRegular_on_quot_iff_lsmul_comap_le, smul_top_le_comap_smul_top, Valuation.leSubmodule_comap_algebraMap_eq_leIdeal, CliffordAlgebra.ΞΉ_range_comap_reverse, iInf_comap_proj, comap_top, LinearMap.quotientInfEquivSupQuotient_symm_apply_right, Module.le_comap_jacobson, comapSubtypeEquivOfLe_symm_apply, comap_bot, Module.End.genEigenspace_restrict, le_comap_range_rTensor, LinearMap.quotientInfEquivSupQuotient_surjective, IsOrtho.comap, Subspace.comap_dualAnnihilator_dualAnnihilator, comap_liftQ, ContinuousLinearEquiv.ofSubmodule'_toContinuousLinearMap, comap_sup_of_injective, comap_unop_mul, disjoint_iff_comap_eq_bot, CliffordAlgebra.submodule_map_involute_eq_comap, LieIdeal.comap_toSubmodule, Module.mapEvalEquiv_symm_apply, LinearMap.ker_le_comap, LinearMap.comap_le_comap_iff, comap_subtype_le_iff, comap_map_eq
|
comapSubtypeEquivOfLe π | CompOp | 2 mathmath: comapSubtypeEquivOfLe_apply_coe, comapSubtypeEquivOfLe_symm_apply
|
compatibleMaps π | CompOp | β |
equivMapOfInjective π | CompOp | 3 mathmath: AffineSubspace.linear_equivMapOfInjective, map_equivMapOfInjective_symm_apply, coe_equivMapOfInjective_apply
|
gciMapComap π | CompOp | β |
giMapComap π | CompOp | β |
map π | CompOp | 323 mathmath: CliffordAlgebra.ΞΉ_range_map_map, LinearPMap.inverse_graph, LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal, LinearMap.iterateRange_succ, comap_equiv_eq_map_symm, LinearMap.map_le_map_iff, Subspace.dualAnnihilator_dualAnnihilator_eq_map, map_comap_eq_of_le, map_dualCoannihilator_le, lift_rank_map_le, LieSubalgebra.mem_map_submodule, RootPairing.rootSpan_dualAnnihilator_le_ker_rootForm, spanRank_map_le, LinearPMap.neg_graph, Ideal.span_pow_eq_map_homogeneousSubmodule, Ideal.span_eq_map_homogeneousSubmodule, LinearEquiv.map_mem_invtSubmodule_conj_iff, map_iSup, LinearMap.iSupIndep_map, fg_map_iff, rank_map_le, map_span_le, comap_map_eq_of_injective, map_comap_eq_self, iSup_map_single_le, LinearIsometry.map_starProjection', LinearMap.map_injective, Module.End.eigenspace_restrict_le_eigenspace, dualAnnihilator_map_dualMap_le, IsLocalRing.map_mkQ_eq, adjoin_monomial_eq_reesAlgebra, LinearMap.submoduleMap_coe_apply, toLinearPMap_range, Ring.jacobson_quotient_of_le, CliffordAlgebra.ΞΉ_range_map_lift, comap_map_sup_of_comap_le, IsOrtho.map_iff, RootPairing.finrank_rootSpan_map_polarization_eq_finrank_corootSpan, equivSubtypeMap_symm_apply, map_comap_eq, map_smul'', map_lt_map_of_le_of_sup_lt_sup, SModEq.map, LinearMap.map_le_map_iff', map_inf_comap_of_surjective, Module.mapEvalEquiv_apply, Valuation.leIdeal_map_algebraMap_eq_leSubmodule_min, Module.map_jacobson_of_bijective, mem_map, LieSubmodule.lie_top_eq_of_span_sup_eq_top, Finsupp.span_image_eq_map_linearCombination, map_id, goursat, comap_iInf_map_of_injective, quotientQuotientEquivQuotientAux_mk, AffineSubspace.map_mk', prod_le_iff, map_top, map_le_map_iff_of_injective, map_unop_mul, LinearIsometry.isComplete_map_iff, codisjoint_map, topologicalClosure_map, LieSubmodule.coe_map_toEnd_le, monomial_mem_adjoin_monomial, inf_genEigenspace, LinearMap.map_coprod_prod, strictMono_comap_prod_map, Module.End.map_genEigenrange_le, RootPairing.corootSpan_map_flip_toPerfPair, map_bot, comap_iSup_map_of_injective, IsLocalRing.map_tensorProduct_mk_eq_top, DenseRange.topologicalClosure_map_submodule, map_sup, LinearMap.IsPerfectCompl.isCompl_right, LieSubmodule.toSubmodule_map, LinearMap.range_comp, FG.map, map_mkQ_eq_top, map_eq_top_iff, snd_map_fst, comap_map_eq_self, Function.Exact.exact_mapQ_iff, map_orthogonal_equiv, differentialIdeal_le_iff, apply_coe_mem_map, mapβ_map_left, LieIdeal.map_toSubmodule, span_algebraMap_image, dualCoannihilator_map_linearEquiv_flip, RootPairing.rootSpan_map_toPerfPair, isCoatom_map_of_ker_le, RootPairing.corootSpan_dualAnnihilator_map_eq, map_inf_eq_map_inf_comap, MvPolynomial.map_restrict_dom_evalβ, snd_map_snd, IsOrtho.map, mapβ_map_right, map_strictMono_of_injective, CliffordAlgebra.submodule_map_pow_reverse, annihilator_map_mkQ_eq_colon, LieSubmodule.mem_baseChange_iff, KaehlerDifferential.ker_map, LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict, CliffordAlgebra.evenOdd_map_reverse, map_unop_pow, CliffordAlgebra.ΞΉ_range_map_reverse, LinearMap.comap_codRestrict, span_image_linearEquiv, comap_sup_map_of_injective, CliffordAlgebra.ΞΉ_range_map_involute, HasOrthogonalProjection.map_linearIsometryEquiv', card_quotient_mul_card_quotient, set_smul_eq_map, map_equiv_traceDual, LinearMap.IsIdempotentElem.commute_iff_of_isUnit, Module.map_jacobson_of_ker_le, map_comp, map_subtype_embedding_eq, exists_dual_map_eq_bot_of_lt_top, baseChange_eq_span, span_algebraMap_image_of_tower, AffineMap.map_vectorSpan, LinearIsometryEquiv.completeSpace_map, disjoint_map, mapβ_span_singleton_eq_map_flip, map_op_pow, starProjection_map_apply, le_comap_map, LinearDisjoint.map, map_subtype_span_singleton, Function.Surjective.lieModule_lcs_map_eq, differentialIdeal_le_fractionalIdeal_iff, comap_inf_map_of_injective, finrank_map_le, map_iInf, singleton_smul, orderIsoMapComap_symm_apply', KaehlerDifferential.kerTotal_map, coe_mulMap_comp_eq, LinearEquiv.submoduleMap_apply, map_mul, IsPrincipal.generator_map_dvd_of_mem, closure_coe_iSup_map_single, map_inr, ZSpan.map, map_equiv_eq_comap_symm, LieIdeal.coe_map_of_surjective, map_le_isotypicComponent, map_strict_mono_of_ker_inf_eq, Subalgebra.map_toSubmodule, comap_map_mkQ, toLinearPMap_domain, Module.End.invtSubmodule.map_subtype_mem_of_mem_invtSubmodule, LinearIsometry.map_starProjection, equivSubtypeMap_apply, map_eq_bot_iff, reflection_map, orderIsoMapComap_apply, AffineSubspace.map_direction, spanRank_map_eq_of_injective, IsPrincipal.map, fst_map_fst, LinearMap.map_span, map_surjective_of_surjective, gc_map_comap, map_symm_eq_iff, map_op_mul, RootPairing.ker_rootForm_eq_dualAnnihilator, RootPairing.range_polarizationIn, iSup_map_single, Module.jacobson_quotient_of_le, LinearMap.prodMap_map_prod, LinearIsometryEquiv.submoduleMap_symm_apply_coe, mapβ_span_singleton_eq_map, fst_map_snd, lt_map_of_comap_lt_of_surjective, map_inf, FractionalIdeal.den_mul_self_eq_num, map_smul', FractionalIdeal.coe_map, WithCStarModule.map_top_submodule, mkQ_map_self, Module.End.mem_invtSubmodule_symm_iff_le_map, map_mapβ, map_pointwise_smul, map_zero, Ideal.map_eq_submodule_map, LinearMap.map_le_range, LinearEquiv.submoduleMap_symm_apply, LinearMap.map_codRestrict, map_inl, AffineSubspace.linear_equivMapOfInjective, Ring.map_jacobson_le, ContinuousLinearMap.IsIdempotentElem.commute_iff_of_isUnit, AddMonoidHom.coe_toIntLinearMap_map, map_unop_one, finrank_map_subtype_eq, reflection_map_apply, map_lt_map_iff_of_injective, coe_mapIic_apply, map_liftQ, CliffordAlgebra.submodule_map_mul_reverse, ContinuousLinearEquiv.submoduleMap_symm_apply, LinearIsometry.completeSpace_map, range_map_nonempty, ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl, toLinearPMap_apply_aux, mulMap_map_comp_eq, map_iSup_comap_of_surjective, map_mono, IsLocalRing.CotangentSpace.map_eq_top_iff, map_iInf_comap_of_surjective, Subspace.map_le_dualAnnihilator_dualAnnihilator, map_comap_eq_of_surjective, RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root', LinearMap.range_domRestrict, LinearEquiv.rank_map_eq, CliffordAlgebra.evenOdd_map_involute, LinearPMap.smul_graph, map_strict_mono_or_ker_sup_lt_ker_sup, KaehlerDifferential.ker_map_of_surjective, map_subtype_top, map_sup_comap_of_surjective, IsFractional.map, ContinuousLinearEquiv.submoduleMap_apply, LinearMap.map_span_le, Module.End.iInf_maxGenEigenspace_restrict_map_subtype_eq, Module.Finite.map, inf_iInf_maxGenEigenspace_of_forall_mapsTo, map_pow, LinearMap.coprod_map_prod, LinearMap.range_eq_map, mem_map_of_mem, orderIsoMapComapOfBijective_apply, map_orthogonal, map_iInf_of_ker_le, CliffordAlgebra.submodule_map_reverse_eq_comap, RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm, LinearMap.map_eq_top_iff, map_range_rTensor_subtype_lid, map_comap_le, FiniteDimensional.instSubtypeMemSubmoduleMap, Module.map_eval_injective, mapHom_apply, LinearMap.BilinForm.toLin_restrict_ker_eq_inf_orthogonal, Finsupp.span_single_image, map_span, prod_map_fst, RootPairing.rootSpan_dualAnnihilator_map_eq, map_comap_subtype, LinearIsometry.isComplete_map_iff', ExteriorAlgebra.ΞΉ_range_map_map, le_map_of_comap_le_of_surjective, map_toAddSubgroup, Ring.map_jacobson_of_ker_le, exists_dual_map_eq_bot_of_notMem, map_le_iff_le_comap, span_image, LinearPMap.graph_map_fst_eq_domain, Module.map_jacobson_le, spanFinrank_map_le_of_fg, IsLocalRing.map_mkQ_eq_top, LinearEquiv.finrank_map_eq, map_covBy_of_injective, map_subtype_range_inclusion, LinearEquiv.lift_rank_map_eq, LinearEquiv.map_mem_invtSubmodule_iff, map_neg, dualAnnihilator_map_linearEquiv_flip_symm, map_coe, le_prod_iff, mapβ_map_map, map_toAddSubmonoid', HasOrthogonalProjection.map_linearIsometryEquiv, topologicalClosure_iSup_map_single, Ideal.map_toCotangent_ker, map_op_one, map_dualCoannihilator_linearEquiv_flip, Subspace.map_dualCoannihilator, ker_liftQ, mem_map_equiv, map_add_le, RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot', map_equivMapOfInjective_symm_apply, map_le_localizedβ, RootPairing.invtSubmodule_reflection_of_invtSubmodule_coreflection, LinearMap.le_ker_iff_map, Module.End.mem_invtSubmodule_iff_map_le, map_one, map_injective_of_injective, RootPairing.ker_corootForm_eq_dualAnnihilator, le_traceDual_iff_map_le_one, KaehlerDifferential.kerTotal_map', mem_graph_toLinearPMap, lieModule_lcs_map_le, LinearMap.IsPerfectCompl.isCompl_left, map_dualAnnihilator_linearEquiv_flip_symm, LinearPMap.graph_map_snd_eq_range, Polynomial.taylorLinearEquiv_apply_coe, map_toAddSubmonoid, map_div, LinearIsometry.submoduleMap_apply_coe, AffineMap.vectorSpan_image_eq_submodule_map, map_inf_le, map_subtype_le, comap_liftQ, coe_equivMapOfInjective_apply, CliffordAlgebra.submodule_map_involute_eq_comap, LinearMap.submoduleMap_surjective, LinearMap.prod_eq_sup_map, map_smul, NonUnitalSubalgebra.map_toSubmodule, surjOn_iff_le_map, prod_map_snd, map_le_smul_top, Finsupp.lmapDomain_supported, quotientQuotientEquivQuotientAux_mk_mk, Polynomial.map_taylorEquiv_degreeLT, restrictScalars_map, LinearIsometryEquiv.submoduleMap_apply_coe, comap_map_eq
|
orderIsoMapComap π | CompOp | 4 mathmath: orderIsoMapComap_apply', orderIsoMapComap_symm_apply', orderIsoMapComap_symm_apply, orderIsoMapComap_apply
|
orderIsoMapComapOfBijective π | CompOp | 2 mathmath: orderIsoMapComapOfBijective_symm_apply, orderIsoMapComapOfBijective_apply
|
submoduleOf π | CompOp | 4 mathmath: submoduleOf_sup_of_le, LinearMap.submoduleOf_span_singleton_of_mem, submoduleOf_eq_top, submoduleOf_self
|
submoduleOfEquivOfLe π | CompOp | β |