Defs

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

Statistics

Metric	Count
Definitions toModule, toModule', add, addCommGroup, addCommMonoid, copy, inhabited, instPartialOrder, module', ofClass, ofLinearComb, setLike, smul, toAddSubgroup, toAddSubmonoid, toSubMulAction, zero, module'	18
Theorems addSubgroupClass, addSubmonoidClass, add_mem, add_mem_iff_left, add_mem_iff_right, carrier_eq_coe, coe_add, coe_copy, coe_eq_zero, coe_mem, coe_mk, coe_neg, coe_ofClass, coe_ofLinearComb, coe_set_mk, coe_smul, coe_smul_of_tower, coe_sub, coe_toAddSubgroup, coe_toAddSubmonoid, coe_toSubMulAction, coe_zero, copy_eq, eta, ext, ext_iff, instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallHSMul, isScalarTower, isScalarTower', mem_carrier, mem_mk, mem_toAddSubgroup, mem_toAddSubmonoid, mk_eq_zero, mk_le_mk, neg_mem, neg_mem_iff, nonempty, smulMemClass, smul_mem, smul_mem', smul_mem_iff', smul_mem_iff'', smul_mem_iff_of_isUnit, smul_of_tower_mem, sub_mem, sub_mem_iff_left, sub_mem_iff_right, toAddSubgroup_inj, toAddSubgroup_injective, toAddSubmonoid_inj, toAddSubmonoid_injective, toSubMulAction_inj, toSubMulAction_injective, zero_mem	55
Total	73

SMulMemClass

Definitions

Name	Category	Theorems
toModule 📖	CompOp	—
toModule' 📖	CompOp	—

Submodule

Definitions

Name	Category	Theorems
add 📖	CompOp	3 math math: coe_add, LinearPMap.map_add, LieModule.Cohomology.add_apply_apply
addCommGroup 📖	CompOp	547 math math: instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe, Rep.resCoindHomEquiv_apply_hom, groupCohomology.instEpiModuleCatH2π, groupHomology.π_comp_H2Iso_hom_assoc, Affine.Simplex.altitudeFoot_restrict, LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, AffineSubspace.coe_vsub, groupHomology.mapCycles₂_comp_assoc, Module.End.isSemisimple_restrict_iff, IsIsotypic.linearEquiv_fun, groupCohomology.toCocycles_comp_isoCocycles₁_hom, Affine.Simplex.orthogonalProjectionSpan_map, EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, groupCohomology.isoCocycles₁_hom_comp_i_apply, IsSemisimpleModule.submodule, AffineMap.restrict.bijective, NumberField.Units.logEmbedding_fundSystem, RootPairing.instIsRootSystemSubtypeMemSubmoduleSpanRangeCoeEmbeddingRootCorootRestrictScalars', Affine.Simplex.finiteDimensional_direction_altitude, IsIsotypic.isotypicComponents, toLinearEquiv_orthogonalDecomposition_symm, NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection, covBy_iff_quot_is_simple, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_apply, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply, groupCohomology.cocyclesIso₀_hom_comp_f, Rep.resCoindAdjunction_counit_app_hom_hom, groupCohomology.H1π_comp_map_assoc, groupHomology.mapCycles₁_comp_apply, Affine.Simplex.restrict_reindex, finiteDimensional_vectorSpan_range, RootPairing.restrictScalars_coe_coroot, groupCohomology.π_comp_H0Iso_hom, Affine.Simplex.faceOppositeCentroid_restrict, groupCohomology.π_comp_H1Iso_hom_assoc, EuclideanGeometry.orthogonalProjection_congr, toLinearEquiv_orthogonalDecomposition, groupCohomology.mapCocycles₂_comp_i, finiteDimensional_direction_affineSpan_of_finite, Module.Basis.ofZLatticeBasis_apply, groupCohomology.H0IsoOfIsTrivial_hom, bot_lt_isotypicComponent, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i_hom, groupCohomology.coe_mapCocycles₁, Affine.Simplex.restrict_map_restrict, EuclideanGeometry.orthogonalProjection_contLinear, EuclideanGeometry.dist_orthogonalProjection_eq_iff_oangle_eq, groupHomology.cyclesMap_comp_isoCycles₂_hom, AffineSubspace.coe_subtypeA, groupHomology.mapCycles₁_comp_assoc, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, AffineSubspace.subtype_apply, Module.Basis.ofZLatticeComap_apply, Module.End.mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo, isIsotypicOfType_submodule_iff, isSemisimple_torsionBy_of_irreducible, eq_isotypicComponent_iff, exteriorPower.alternatingMapLinearEquiv_ιMulti, groupHomology.δ₀_apply, Module.End.eigenspace_restrict_le_eigenspace, EuclideanGeometry.reflection_vadd_smul_vsub_orthogonalProjection, groupHomology.isoCycles₁_inv_comp_iCycles_apply, eq_isotypicComponent_of_le, groupCohomology.map_H0Iso_hom_f_apply, EuclideanGeometry.inter_eq_singleton_orthogonalProjection, groupCohomology.H0IsoOfIsTrivial_inv_apply, groupHomology.chains₁ToCoinvariantsKer_surjective, AffineSubspace.linear_topEquiv, Affine.Simplex.orthogonalProjectionSpan_eq_point, isSimpleModule_iff_isAtom, FiniteDimensional.span_of_finite, Rep.resCoindAdjunction_unit_app_hom_hom, RootPairing.restrictScalars_pairing, EuclideanGeometry.orthogonalProjection_map, exteriorPower.alternatingMapLinearEquiv_symm_map, Affine.Simplex.circumradius_restrict, Affine.Simplex.medial_restrict, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, coe_orthogonalDecomposition_symm, groupCohomology.mapCocycles₂_comp_i_apply, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_apply, ZLattice.module_finite, EuclideanGeometry.angle_orthogonalProjection_self, EuclideanGeometry.orthogonalProjection_apply_mem, groupHomology.cycles₁IsoOfIsTrivial_hom_apply, AffineSubspace.coe_subtypeₐᵢ, PeriodPair.latticeBasis_zero, EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq, RootPairing.finrank_corootSpanIn_int, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, groupCohomology.mapCocycles₂_comp_i_assoc, ZLattice.rank, Subspace.finiteDimensional_quot_dualCoannihilator_iff, groupCohomology.H1IsoOfIsTrivial_inv_apply, groupHomology.mapCycles₁_id_comp_assoc, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, goursat, groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, groupCohomology.H2π_comp_map_apply, groupHomology.mapCycles₁_comp, finiteDimensional_vectorSpan_image_of_finite, Affine.Simplex.ninePointCircle_restrict, groupCohomology.toCocycles_comp_isoCocycles₂_hom, length_lt, ModuleCat.imageIsoRange_hom_subtype, groupHomology.mapCycles₁_comp_i, Affine.Simplex.face_restrict, groupCohomology.shortComplexH0_f, Affine.Simplex.interior_restrict, RootPairing.finrank_rootSpanIn_int, AffineSubspace.inclusion_linear, HasStrictFDerivAt.to_implicitFunctionOfComplemented, EuclideanGeometry.orthogonalProjection_apply', Affine.Simplex.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, Rep.subtype_hom, inf_genEigenspace, finiteDimensional_sup, isIsotypic_submodule_iff, finiteDimensional_direction_map, groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply, ModuleCat.imageIsoRange_inv_image_ι_apply, EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_le, EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, FiniteDimensional.span_finset, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, IsIsotypic.isotypicComponent, LinearMap.restrict_sub, Rep.invariantsAdjunction_unit_app, groupHomology.mapCycles₂_id_comp, ZLattice.comap_equiv_apply, Module.Basis.addSubgroupOfClosure_repr_apply, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, Module.length_top, groupCohomology.H2π_eq_iff, NumberField.det_basisOfFractionalIdeal_eq_absNorm, GradedTensorProduct.auxEquiv_comm, LinearMap.comap_leq_ker_subToSupQuotient, groupCohomology.δ₁_apply, groupHomology.toCycles_comp_isoCycles₁_hom_apply, IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp, Affine.Simplex.altitude_restrict_eq_comap_subtype, AffineSubspace.isometryEquivMap.toAffineMap_eq, groupHomology.mapCycles₂_comp_i, AffineSubspace.signedInfDist_eq_signedDist_of_mem, groupCohomology.map_H0Iso_hom_f, Affine.Simplex.signedInfDist_apply_self, LinearMap.quotientInfEquivSupQuotient_apply_mk, finiteDimensional_vectorSpan_of_finite, finiteQuotient_iff, groupCohomology.π_comp_H1Iso_hom, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, Module.End.eigenspace_restrict_eq_bot, AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection, NumberField.mixedEmbedding.span_idealLatticeBasis, AffineEquiv.linear_ofEq, instPolynormableSpaceSubtypeMemSubmodule, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc_apply, Collinear.finiteDimensional_direction_affineSpan, finiteDimensional_direction_affineSpan_insert_set, Affine.Simplex.orthogonalProjectionSpan_congr, Polynomial.adjSylvester_comp_sylveserMap, groupHomology.mapCycles₁_id_comp_apply, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_assoc, CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, Ideal.quotientToQuotientRangePowQuotSucc_mk, Module.End.IsSemisimple.restrict, groupCohomology.instEpiModuleCatH1π, Coplanar.finiteDimensional_direction_affineSpan, IsSemisimpleModule.sup, Affine.Simplex.ExcenterExists.touchpointWeights_restrict, groupCohomology.H2π_comp_map, CharacterModule.intSpanEquivQuotAddOrderOf_apply, groupHomology.π_comp_H2Iso_hom, AffineSubspace.instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection, groupHomology.mapCycles₁_comp_i_apply, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupHomology.mapCycles₂_comp, ModuleCat.kernelIsoKer_inv_kernel_ι_apply, IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite, groupCohomology.isoCocycles₂_hom_comp_i, EuclideanGeometry.orthogonalProjection_subtype, coe_orthogonalDecomposition, EuclideanGeometry.two_zsmul_oangle_self_orthogonalProjection, groupCohomology.π_comp_H0Iso_hom_apply, finiteDimensional_direction_affineSpan_insert, groupHomology.coe_mapCycles₂, groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply, groupHomology.H1π_comp_map_apply, Affine.Simplex.ExcenterExists.excenter_restrict, finiteDimensional_direction_affineSpan_range, Polynomial.det_taylorLinearEquiv_toLinearMap, EuclideanGeometry.orthogonalProjection_vadd_eq_self, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, Module.length_submodule, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, groupCohomology.mapCocycles₁_one, EuclideanGeometry.oangle_orthogonalProjection_self, Affine.Simplex.map_altitude_restrict, Affine.Simplex.faceOpposite_restrict, groupHomology.H2π_comp_map_assoc, finiteDimensional_vectorSpan_insert_set, LinearMap.quotientInfEquivSupQuotient_injective, EuclideanGeometry.dist_orthogonalProjection_eq_dist_iff_eq_of_mem, GradedTensorProduct.auxEquiv_mul, AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert, Affine.Simplex.exradius_restrict, finiteDimensional_vectorSpan_singleton, finiteDimensional_inf_right, groupCohomology.π_comp_H0Iso_hom_assoc, ModuleCat.imageIsoRange_hom_subtype_assoc, ZLattice.module_free, Affine.Simplex.orthogonalProjection_circumcenter, groupCohomology.H2π_comp_map_assoc, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, groupHomology.mapCycles₂_comp_apply, AffineSubspace.subtypeA_toAffineMap, Affine.Simplex.exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter, Rep.coindFunctorIso_inv_app_hom_hom_apply_coe, instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent, HasStrictFDerivAt.to_implicitFunction, natAbs_det_equiv, Module.End.IsFinitelySemisimple.restrict, Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq, groupHomology.H2π_eq_iff, le_isotypicComponent, groupHomology.H1AddEquivOfIsTrivial_single, Ideal.quotientToQuotientRangePowQuotSucc_surjective, groupHomology.isoCycles₂_hom_comp_i_apply, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, Module.length_bot, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, AffineSubspace.coe_vadd, groupCohomology.isoCocycles₁_inv_comp_iCocycles, Affine.Simplex.circumcenter_restrict, instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy, AffineMap.restrict.injective, Affine.Simplex.height_restrict, ModuleCat.imageIsoRange_inv_image_ι, instModuleFinite_of_discrete_submodule, EuclideanGeometry.orthogonalProjection_affineSpan_singleton, groupHomology.cyclesMap_comp_isoCycles₂_hom_assoc, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom, AffineSubspace.subtype_injective, Module.End.isFinitelySemisimple_iff', AffineSubspace.subtype_linear, GradedTensorProduct.mulHom_apply, EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, AffineSubspace.topEquiv_symm_apply_coe, sndL_comp_coe_orthogonalDecomposition, IsSemisimpleModule.sSup_simples_le, IsSemisimpleModule.exists_simple_submodule, groupHomology.mapCycles₂_id_comp_assoc, groupHomology.π_comp_H1Iso_hom_apply, Rep.coindIso_inv_hom_hom, map_le_isotypicComponent, Collinear.finiteDimensional_vectorSpan, groupCohomology.map_id_comp_H0Iso_hom_apply, groupCohomology.subtype_comp_d₀₁_assoc, groupHomology.toCycles_comp_isoCycles₂_hom, groupCohomology.map_id_comp_H0Iso_hom, groupHomology.cyclesMap_comp_isoCycles₂_hom_apply, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc_apply, torsionBy.mk_ideal_smul, Affine.Simplex.incenter_restrict, groupHomology.mapCycles₁_id_comp, groupCohomology.cocycles₁IsoOfIsTrivial_inv_hom_apply_coe, EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection, PeriodPair.latticeBasis_one, ZLattice.covolume_eq_det_mul_measureReal, Affine.Simplex.orthogonalProjectionSpan_faceOpposite_eq_point_rev, EuclideanGeometry.dist_orthogonalProjection_eq_infNndist, FiniteDimensional.finiteDimensional_submodule, Ideal.toCotangent_apply, groupHomology.isoCycles₁_hom_comp_i_apply, AffineMap.restrict.surjective, Affine.Simplex.inradius_restrict, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, ZLattice.exists_forall_abs_repr_le_norm, AffineMap.restrict.coe_apply, ModuleCat.imageIsoRange_inv_image_ι_assoc, IsSemisimpleModule.sSup_simples_eq_top, groupCohomology.H1π_eq_zero_iff, NumberField.fractionalIdeal_rank, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_apply, ModuleCat.kernelIsoKer_hom_ker_subtype, groupHomology.H1ToTensorOfIsTrivial_H1π_single, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc_apply, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangent, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, Ideal.quotientToQuotientRangePowQuotSucc_injective, groupCohomology.cocyclesMk₁_eq, Subalgebra.finiteDimensional_toSubmodule, EuclideanGeometry.orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem, Rep.quotientToInvariantsFunctor_obj_V, IsSemisimpleModule.exists_end_ringEquiv, RootPairing.restrictScalars_coe_root, exteriorPower.presentation_relation, EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq, Affine.Simplex.centroid_restrict, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_apply, groupHomology.cyclesMap_comp_isoCycles₁_hom_apply, groupHomology.toCycles_comp_isoCycles₂_hom_apply, groupCohomology.H2π_eq_zero_iff, Coplanar.finiteDimensional_vectorSpan, groupCohomology.mapCocycles₁_comp_i_assoc, groupCohomology.H1π_comp_map_apply, PeriodPair.latticeEquiv_symm_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, EuclideanGeometry.dist_orthogonalProjection_eq_infDist, EuclideanGeometry.orthogonalProjection_mem, groupCohomology.π_comp_H2Iso_hom_assoc, Affine.Simplex.orthogonalProjectionSpan_restrict, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, IsSemisimpleModule.exists_end_algEquiv, Affine.Simplex.setInterior_restrict, AffineSubspace.finiteDimensional_sup, groupHomology.mapCycles₂_hom, groupHomology.isoCycles₂_inv_comp_iCycles_apply, Affine.Simplex.excenterWeights_restrict, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff, AffineEquiv.ofEq_symm, ModuleCat.kernelIsoKer_hom_ker_subtype_apply, ZLattice.abs_repr_lt_of_norm_lt, EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq, groupHomology.cyclesMk₂_eq, AffineSubspace.linear_equivMapOfInjective, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_assoc, EuclideanGeometry.Sphere.IsTangentAt.eq_orthogonalProjection, groupHomology.H1π_eq_zero_iff, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, groupHomology.π_comp_H1Iso_hom_assoc, Affine.Simplex.median_restrict, groupHomology.H2π_comp_map, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_apply, affineSpan_coe_preimage_eq_top, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff, groupHomology.H1π_comp_map_assoc, Ideal.natAbs_det_equiv, EuclideanGeometry.reflection_eq_iff_orthogonalProjection_eq, groupHomology.instEpiModuleCatH1π, Affine.Simplex.closedInterior_restrict, groupCohomology.isoCocycles₂_inv_comp_iCocycles, EuclideanGeometry.orthogonalProjection_orthogonalProjection, groupCohomology.δ₀_apply, EuclideanGeometry.orthogonalProjection_vsub_mem_direction, exteriorPower.presentation_R, finiteDimensional_direction_affineSpan_image_of_finite, groupHomology.instEpiModuleCatH2π, NumberField.mem_span_basisOfFractionalIdeal, Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq, AffineSubspace.topEquiv_apply, groupCohomology.cocyclesMk₂_eq, Affine.Simplex.mongePoint_restrict, mem_isotypicComponents_iff, groupHomology.H1π_comp_map, Affine.Simplex.eulerPoint_restrict, EuclideanGeometry.vsub_orthogonalProjection_mem_direction, AffineSubspace.coe_inclusion_apply, groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply, Affine.Simplex.ExcenterExists.touchpoint_restrict, Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection, IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite, groupHomology.cyclesMk₁_eq, groupHomology.mapCycles₂_comp_i_assoc, Affine.Simplex.excenterWeightsUnnorm_restrict, groupCohomology.isoCocycles₁_hom_comp_i, EuclideanGeometry.Sphere.IsTangent.isTangentAt, groupCohomology.mapCocycles₁_comp_i_apply, Rep.coindMap_hom, groupHomology.mapCycles₂_id_comp_apply, Polynomial.det_taylorLinearEquiv, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end, groupHomology.H2π_comp_map_apply, EuclideanGeometry.reflection_apply', EuclideanGeometry.oangle_self_orthogonalProjection, le_isotypicComponent_iff, Projectivization.instFiniteDimensionalSubtypeMemSubmoduleSubmodule, fg_iff_finiteDimensional, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_K, LinearMap.coe_quotientInfToSupQuotient, MatrixModCat.toModuleCat_map, AffineEquiv.coe_ofEq_apply, finiteDimensional_bot, groupCohomology.π_comp_H2Iso_hom_apply, CliffordAlgebra.even.lift.aux_apply, instIsSemisimpleModuleSubtypeMemSubmoduleValSetIsotypicComponents, AffineMap.restrict.linear, Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, AffineSubspace.coe_subtype, groupHomology.isoCycles₁_hom_comp_i_assoc, FractionalIdeal.abs_det_basis_change, Rep.invariantsFunctor_map_hom, Module.End.iInf_maxGenEigenspace_restrict_map_subtype_eq, Affine.Simplex.orthogonalProjectionSpan_reindex, groupCohomology.π_comp_H1Iso_hom_apply, topologicalAddGroup, inf_iInf_maxGenEigenspace_of_forall_mapsTo, RootPairing.restrictScalars_toLinearMap_apply_apply, fstL_comp_coe_orthogonalDecomposition, EuclideanGeometry.orthogonalProjection_linear, AffineSubspace.signedInfDist_def, IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top, NumberField.Units.unitLattice_rank, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_apply, groupHomology.π_comp_H2Iso_hom_apply, instIsSimpleModuleSubtypeMemSubmoduleValSetSetOfNonemptyLinearEquivId, MatrixModCat.toModuleCat_obj_isAddCommGroup, Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle, ZLattice.normBound_spec, groupHomology.mapCycles₁_hom, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π_hom, groupHomology.isoCycles₁_inv_comp_iCycles, Affine.Simplex.signedInfDist_affineCombination, groupHomology.cyclesMap_comp_isoCycles₁_hom_assoc, EuclideanGeometry.angle_self_orthogonalProjection, groupHomology.coe_mapCycles₁, NumberField.Units.logEmbeddingEquiv_apply, groupHomology.toCycles_comp_isoCycles₁_hom, NumberField.basisOfFractionalIdeal_apply, Module.Basis.ofZLatticeComap_repr_apply, groupHomology.mapCycles₂_comp_i_apply, EuclideanGeometry.orthogonalProjection_eq_self_iff, groupCohomology.cocyclesIso₀_hom_comp_f_apply, groupCohomology.subtype_comp_d₀₁, EuclideanGeometry.reflection_subtype, LinearMap.det_eq_det_mul_det, FiniteDimensional.instSubtypeMemSubmoduleMap, groupHomology.isoCycles₂_hom_comp_i, groupHomology.π_comp_H1Iso_hom, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_H, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc_apply, groupHomology.isoCycles₂_inv_comp_iCycles, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_apply, Module.Basis.ofZLatticeBasis_repr_apply, groupHomology.mkH1OfIsTrivial_apply, IsIsotypic.linearEquiv_finsupp, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom, AffineSubspace.inclusion_rfl, IsSemisimpleModule.eq_bot_or_exists_simple_le, NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, CharacterModule.intSpanEquivQuotAddOrderOf_apply_self, AddSubgroup.relIndex_eq_natAbs_det, groupHomology.π_comp_H1Iso_inv_apply, LinearMap.quotientInfEquivSupQuotient_symm_apply_left, sSup_simples_eq_top_iff_isSemisimpleModule, exteriorPower.presentation_var, groupCohomology.isoCocycles₂_hom_comp_i_apply, torsionBySet.mk_smul, EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal, Module.End.genEigenspace_restrict_eq_top, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc_apply, groupHomology.cycles₁IsoOfIsTrivial_inv_apply, FiniteDimensional.subalgebra_toSubmodule, EuclideanGeometry.eq_orthogonalProjection_of_eq_subspace, EuclideanGeometry.orthogonalProjection_apply, groupHomology.isoCycles₁_hom_comp_i, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, AffineSubspace.signedInfDist_apply_self, EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection, EuclideanGeometry.orthogonalProjection_mem_orthogonal, exteriorPower.presentation_G, groupCohomology.H1π_comp_map, groupCohomology.cocyclesMk₀_eq, EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self, NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype, IsSemisimpleModule.exists_linearEquiv_dfinsupp, ModuleCat.mono_as_hom'_subtype, AffineSubspace.equivMapOfInjective_toFun, exteriorPower.ιMulti_family_span, Ideal.quotientToQuotientRangePowQuotSuccAux_mk, ZLattice.sum_piFinset_Icc_rpow_le, EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem, isFullyInvariant_iff_le_imp_isotypicComponent_le, Affine.Simplex.map_subtype_restrict, Affine.Simplex.restrict_map_subtype, groupCohomology.map_H0Iso_hom_f_assoc, ModuleCat.kernelIsoKer_inv_kernel_ι, IsIsotypicOfType.isotypicComponent, instModuleFree_of_discrete_submodule, Ideal.natAbs_det_basis_change, ModuleCat.imageIsoRange_hom_subtype_apply, finiteDimensional_of_le, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, IsSemisimpleModule.range, LinearMap.quotientInfEquivSupQuotient_symm_apply_right, Affine.Simplex.restrict_map_inclusion, finiteDimensional_direction_affineSpan_singleton, EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq, groupCohomology.map_id_comp_H0Iso_hom_assoc, Module.End.genEigenspace_restrict, groupCohomology.isoCocycles₂_hom_comp_i_assoc, EuclideanGeometry.orthogonalProjection_eq_iff_mem, EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq, Rep.coindIso_hom_hom_hom, groupCohomology.coe_mapCocycles₂, LinearMap.quotientInfEquivSupQuotient_surjective, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_assoc, groupCohomology.H1π_eq_iff, Module.Basis.addSubgroupOfClosure_apply, groupCohomology.isoCocycles₁_hom_comp_i_assoc, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt, groupHomology.mapCycles₁_quotientGroupMk'_epi, groupHomology.mapCycles₁_comp_i_assoc, AffineEquiv.ofEq_rfl, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_apply, LinearMap.finiteDimensional_range, torsionBy.mk_smul, groupHomology.π_comp_H2Iso_inv_apply, EuclideanGeometry.dist_set_eq_iff_dist_orthogonalProjection_eq, finiteDimensional_inf_left, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, groupCohomology.mapCocycles₁_comp_i, PeriodPair.finrank_lattice, hasFDerivAt_stereoInvFunAux_comp_coe, finiteDimensional_vectorSpan_insert, groupHomology.isoCycles₂_hom_comp_i_assoc, Int.submodule_toAddSubgroup_index_ne_zero_iff, groupCohomology.π_comp_H2Iso_hom, FiniteDimensional.span_singleton, groupHomology.H2π_eq_zero_iff, ZLattice.exists_finsetSum_norm_rpow_le_tsum, Affine.Simplex.restrict_points_coe, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, ZLattice.abs_repr_le, Affine.Simplex.excenterExists_restrict, ZLattice.covolume_eq_det, groupHomology.δ₁_apply, EuclideanGeometry.orthogonalProjection_mem_subspace_eq_self, natAbs_det_basis_change, groupHomology.H1π_eq_iff, isSemisimpleModule_iff_exists_linearEquiv_dfinsupp, groupHomology.cyclesMap_comp_isoCycles₁_hom, HahnEmbedding.Partial.toOrderAddMonoidHom_injective
addCommMonoid 📖	CompOp	1213 math math: DirectSum.IsInternal.ofBijective_coeLinearMap_same, TensorProduct.mapInclIsometry_apply, coe_sum, finrank_sup_add_finrank_inf_eq, Ideal.toCotangent_to_quotient_square, LinearMap.lTensor_ker_subtype_tensorKerEquiv_symm, DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply, instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe, KaehlerDifferential.kerCotangentToTensor_toCotangent, Rep.resCoindHomEquiv_symm_apply_hom, Polynomial.degreeLT.addLinearEquiv_symm_apply_inr, Rep.invariantsAdjunction_homEquiv_symm_apply_hom, TensorProduct.forall_vanishesTrivially_iff_forall_fg_rTensor_injective, LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal, LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, rTensorOne_symm_apply, iSupIndep.linearEquiv_symm_apply, topEquiv_symm_apply_coe, iSupIndep.dfinsupp_lsum_injective, FG.rTensor.directedSystem, Algebra.idealMap_eq_ofEq_comp_toLocalized₀, coe_continuous_linearProjOfClosedCompl', RootPairing.posRootForm_posForm_apply_apply, Ideal.selfBasis_def, Module.Basis.mem_submodule_iff, LinearMap.BilinForm.dualSubmoduleToDual_apply_apply, OrthonormalBasis.orthogonalProjection_eq_sum, IsIsotypic.linearEquiv_fun, finrank_span_finset_eq_card, derivationToSquareZeroOfLift_apply, finrank_span_set_eq_card, linearProjOfIsCompl_apply_left, subtype_comp_inclusion, Algebra.Extension.Cotangent.span_eq_top_of_span_eq_ker, MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum, IsSemisimpleModule.exists_submodule_linearEquiv_quotient, LinearMap.BilinForm.dualSubmoduleToDual_injective, ExteriorAlgebra.GradedAlgebra.liftι_eq, RootPairing.root'In_corootSpanMem_eq_pairingIn, RootPairing.rootForm_restrict_nondegenerate_of_ordered, Polynomial.degreeLT.instFreeSubtypeMemSubmodule, finrank_add_finrank_le_of_disjoint, orthogonalDecomposition_symm_apply, Ideal.finrank_eq_finrank, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, LinearMap.subtype_comp_codRestrict, exteriorPower.basis_apply, LinearMap.IsProj.subtype_comp_codRestrict, NumberField.Units.logEmbedding_fundSystem, Ideal.exists_smith_normal_form, toIsOrderedAddMonoid, LinearMap.subtype_comp_restrict, LinearMap.IsProj.codRestrict_apply_cod, Finsupp.restrictDom_apply, rank_le_card_isVisible, RootPairing.RootPositiveForm.zero_lt_posForm_apply_root, exteriorPower.linearMap_ext_iff, Ideal.toCotangent_eq, RootPairing.finrank_corootSpan_eq', mulMap_tmul, comm_trans_lTensorOne, isNoetherian_submodule_right, Polynomial.toMatrix_sylvesterMap', exists_fg_le_eq_rTensor_inclusion, LinearMap.IsRefl.domRestrict, TensorProduct.range_mapIncl, LinearMap.BilinForm.ker_restrict_eq_of_codisjoint, toLinearEquiv_orthogonalDecomposition_symm, NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, Module.End.isNilpotent_restrict_genEigenspace_nat, LinearMap.injective_restrict_iff_disjoint, covBy_iff_quot_is_simple, lift_rank_map_le, MeasureTheory.norm_condExpL2_le, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, tensorEquivSpan_apply_tmul, linearMap_eq_zero_iff_of_eq_span, ContinuousLinearMap.ker_codRestrict, Finsupp.supportedEquivFinsupp_symm_single, LinearDisjoint.not_linearIndependent_pair_of_flat_left, Rep.coindToInd_of_support_subset_orbit, re_inner_starProjection_eq_normSq, DirectSum.decomposeAlgEquiv_symm_apply, LinearMap.le_ker_iff_comp_subtype_eq_zero, MeasureTheory.inner_condExpL2_left_eq_right, linearEquiv_of_le_sSup, linearProjOfIsCompl_apply_right, prodEquivOfIsCompl_symm_apply_snd_eq_zero, exteriorPower.coe_basis, LinearMap.tensorKer_tmul, LinearMap.IsSymmetric.diagonalization_apply_self_apply, finrank_vectorSpan_image_finset_le, Subspace.dualLift_of_subtype, mulMap_one_right_eq, exteriorPower.ιMulti_family_linearIndependent_field, ContinuousLinearEquiv.snd_equivOfRightInverse, span_setOf_mem_eq_top, toLinearEquiv_orthogonalDecomposition, LinearPMap.mk_apply, MeasureTheory.condExpL2_ae_eq_zero_of_ae_eq_zero, Subspace.dualRestrict_comp_dualLift, dualQuotEquivDualAnnihilator_apply, ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm, LinearIndependent.linearCombination_repr, exteriorPower.basis_repr_ne, orthogonalProjection_mem_subspace_eq_self, LinearMap.range_domRestrict_le_range, Module.Basis.mk_repr, LinearMap.submoduleComap_apply_coe, Module.Flat.ker_lTensor_eq, KaehlerDifferential.cotangentComplexBaseChange_tmul, Module.Basis.ofZLatticeBasis_apply, LinearMap.ofIsCompl_smul, quotDualCoannihilatorToDual_apply, injective_inclusionSpan, IsLattice.rank', dualPairing_apply, LinearMap.tensorEqLocusEquiv_apply, LinearMap.domRestrict'_apply, RootPairing.range_polarization_domRestrict_le_span_coroot, RootPairing.finrank_range_polarization_eq_finrank_span_coroot, finrank_vectorSpan_le_iff_not_affineIndependent, groupCohomology.coboundariesToCocycles₁_apply, LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, Module.Basis.ofZLatticeComap_apply, le_linearEquiv_of_sSup_eq_top, FG.lTensor.directedSystem, Module.Basis.coe_mkFinConsOfLE, rank_map_le, LinearMap.tensorKer_coe, LinearMap.BilinForm.restrict_nondegenerate_orthogonal_spanSingleton, Module.End.mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo, finrank_quotient_add_finrank, isIsotypicOfType_submodule_iff, val_mulMap'_tmul, SimpleGraph.card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix, RootPairing.coroot'In_rootSpanMem_eq_pairingIn, exteriorPower.alternatingMapLinearEquiv_ιMulti, KaehlerDifferential.kerToTensor_apply, coe_subtypeL', Polynomial.degreeLT.basis_val, selfAdjointPart_comp_subtype_skewAdjoint, setBasisOfLinearIndependentOfCardEqFinrank_repr_apply, IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule, Algebra.Presentation.differentials.hom₁_single, LinearMap.rank_eq_of_surjective, TensorProduct.quotientTensorQuotientEquiv_symm_apply_mk_tmul, Algebra.Generators.exists_presentation_of_basis_cotangent, lift_rank_range_of_injective, Ideal.mem_toCotangent_ker, isArtinian_iff_submodule_quotient, Module.End.eigenspace_restrict_le_eigenspace, LinearMap.IsSymmetric.directSum_decompose_apply, linearProjOfIsCompl_comp_surjective_of_exact, dualCopairing_eq, Ideal.finsuppTotal_apply_eq_of_fintype, rank_span_set, RootPairing.RootPositiveForm.zero_lt_posForm_iff, quotDualCoannihilatorToDual_nondegenerate, rank_bot, LinearMap.submoduleMap_coe_apply, Algebra.Extension.lTensor_cotangentComplex_eq_cotangentComplexBaseChange, AffineSubspace.linear_topEquiv, toLinearPMap_range, LieHom.quotKerEquivRange_toFun, MeasureTheory.MemLp.condExpL2_ae_eq_condExp, TensorProduct.map₂_eq_range_lift_comp_mapIncl, LinearMap.exists_basis_basis_of_span_eq_top_of_mem_algebraMap, isArtinian_of_le, exteriorPower.ιMulti_span_of_span, biSup_comap_subtype_eq_top, LinearPMap.adjointAux_unique, FractionalIdeal.isNoetherian_coeIdeal, RootPairing.injOn_dualMap_subtype_span_root_coroot, LinearMap.range_domRestrict_eq_range_iff, Ideal.finsuppTotal_apply, TensorProduct.exists_finite_submodule_of_finite', biSup_eq_range_dfinsupp_lsum, IsOrtho.orthogonalProjection_comp_subtypeL, IsIsotypic.submodule_linearEquiv_fun, LieModule.Cohomology.d₂₃_apply, LieAlgebra.InvariantForm.restrict_nondegenerate, exteriorPower.alternatingMapLinearEquiv_symm_map, span_range_inclusion_restrictScalars_eq_top, isNoetherian_submodule, selfAdjointPart_comp_subtype_selfAdjoint, exteriorPower.instFree, HahnEmbedding.Partial.truncLT_mem_range_extendFun, mulMap_comm, Module.Flat.out, RootPairing.finrank_rootSpan_map_polarization_eq_finrank_corootSpan, LieModule.Cohomology.d₁₂_apply_apply, equivSubtypeMap_symm_apply, botEquivPUnit_apply, LinearMap.ofIsComplProd_apply, AffineIndependent.finrank_vectorSpan_add_one, coe_orthogonalDecomposition_symm, Projectivization.finrank_submodule, ker_subtype, MeasureTheory.aestronglyMeasurable_condExpL2, orthogonalProjection_bot, linearProjOfIsCompl_apply_right', ZLattice.module_finite, EuclideanGeometry.orthogonalProjection_apply_mem, LinearMap.restrict_comp, isNoetherian_of_le, IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite, coe_isComplEquivProj_symm_apply, finrank_add_inf_finrank_orthogonal, LieAlgebra.bracket_ofTwoCocycle, LinearMap.exact_subtype_mkQ, Algebra.Extension.Cotangent.val_mk, PeriodPair.latticeBasis_zero, linearDisjoint_iff, GradedTensorProduct.auxEquiv_one, toLocalized₀_apply_coe, LinearMap.IsSymm.domRestrict, Subspace.finrank_dualCoannihilator_eq, sup_eq_range, MeasureTheory.condExpL2_indicator_ae_eq_smul, exteriorPower.ιMultiDual_apply_diag, Representation.instIsTrivialSubtypeMemSubgroupSubmoduleInvariantsCompLinearMapIdSubtypeToInvariants, RootPairing.finrank_corootSpanIn_int, LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_right, Algebra.TensorProduct.linearEquivIncludeRange_toLinearMap, retractionOfSectionOfKerSqZero_comp_kerToTensor, DirectSum.IsInternal.collectedBasis_coe, rank_quotient_add_rank, Ideal.toCotangent_range, RootPairing.RootPositiveForm.posForm_apply_root_root_le_zero_iff, Module.Invertible.exists_linearEquiv_ideal, ZLattice.rank, LinearIndependent.repr_eq_single, FirstOrder.Field.lift_genericMonicPoly, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField, rank_submodule_le_one_iff, AffineIndependent.card_le_finrank_succ, Coplanar.finrank_le_two, Algebra.Generators.exists_presentation_of_free_cotangent, goursat, coe_prodEquivOfIsCompl', Affine.Simplex.finrank_direction_altitude, HahnEmbedding.Seed.strictMono_coeff, Module.Basis.sumQuot_repr_left, LinearEquiv.ofSubmodules_apply, LinearMap.lTensor_range, topEquiv_apply, Polynomial.degreeLT.addLinearEquiv_castAdd, subtype_apply, Ideal.powQuotSuccInclusion_apply_coe, LinearEquiv.toSpanNonzeroSingleton_homothety, MeasureTheory.integral_condExpL2_eq, IsCompactOperator.restrict', RootPairing.instFiniteSubtypeMemSubmoduleRootSpanOfFinite, orzechProperty_iff, LinearMap.tensorKerEquivOfSurjective_symm_tmul, Module.End.pow_restrict, LinearMap.IsProj.eq_conj_prodMap, LinearMap.tensorEqLocus_coe, LinearDisjoint.not_linearIndependent_pair_of_flat_right, finrank_lt_finrank_of_lt, LinearMap.mem_submoduleImage_of_le, Polynomial.degreeLT.addLinearEquiv_apply_fst, mulLeftMap_apply, LinearMap.restrict_commute, MeasureTheory.setIntegral_condExpL2_indicator, OrthonormalBasis.orthogonalProjection_apply_eq_sum, LinearMap.toKerLocalized_isLocalizedModule, submoduleOf_sup_of_le, rank_range_le, DirectSum.coeLinearMap_of, ContinuousLinearMap.coe_equivRange, rank_le, coe_prodEquivOfIsCompl, DirectSum.coeLinearMap_eq_dfinsuppSum, RootPairing.polarizationIn_Injective, finrank_vectorSpan_insert_le, Subspace.dualPairing_nondegenerate, ExteriorAlgebra.GradedAlgebra.ι_sq_zero, RootPairing.finrank_rootSpanIn_int, AddMonoidAlgebra.decomposeAux_coe, LinearMap.ker_rangeRestrict, LinearMap.IsSymmetric.card_filter_eigenvalues_eq, LinearMap.compMultilinearMap_codRestrict, Module.Flat.iff_rTensor_injective, EuclideanGeometry.orthogonalProjection_apply', MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le, Rep.coindVEquiv_symm_apply_coe, Ideal.map_includeRight_eq, inf_genEigenspace, torsionBy_torsionBy_eq_top, TensorProduct.exists_finite_submodule_left_of_setFinite, TensorProduct.quotientTensorEquiv_symm_apply_mk_tmul, LinearEquiv.mem_dilatransvections_iff_rank, basisOfLinearIndependentOfCardEqFinrank_repr_apply, strictMono_comap_prod_map, Matrix.cRank_toNat_eq_finrank, RootPairing.PolarizationIn_eq, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, Module.Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul, dualRestrict_ker_eq_dualAnnihilator, Subalgebra.finrank_toSubmodule, MeasureTheory.norm_condExpL2_coe_le, isArtinian_span_of_finite, MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, LinearMap.finrank_range_of_inj, LinearMap.restrict_sub, coe_linearProjOfIsCompl_apply, inclusion_apply, LinearEquiv.ofLeftInverse_symm_apply, LinearMap.range_rangeRestrict, isNoetherian_iff_submodule_quotient, ZLattice.comap_equiv_apply, surjective_tensorToSpan, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, torsion_torsion_eq_top, finrank_span_le_card, isLocalizedModule, range_subtypeL, botEquivPUnit_symm_apply, Module.Basis.addSubgroupOfClosure_repr_apply, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, span_range_inclusion_eq_top, GradedTensorProduct.auxEquiv_symm_one, NumberField.det_basisOfFractionalIdeal_eq_absNorm, GradedTensorProduct.auxEquiv_comm, LinearMap.comap_leq_ker_subToSupQuotient, HilbertBasis.hasSum_orthogonalProjection, LinearMap.rTensor_injective_iff_subtype, collinear_iff_finrank_le_one, LinearMap.subtype_compAlternatingMap_codRestrict, LinearMap.submoduleImage_apply_of_le, LinearRecurrence.solSpace_rank, LinearEquiv.ofSubmodule'_symm_apply, MeasureTheory.lintegral_nnnorm_condExpL2_le, exteriorPower.finrank_eq, Polynomial.degreeLT.addLinearEquiv_apply_snd, LinearMap.finrank_genEigenspace_le, Module.Basis.sumQuot_repr_inl, LinearMap.IsSymmetric.diagonalization_symm_apply, ContinuousLinearMap.coe_codRestrict, LieModule.weight_vector_multiplication, LinearMap.quotientInfEquivSupQuotient_apply_mk, SimpleGraph.linearIndependent_lapMatrix_ker_basis_aux, finiteQuotient_iff, exteriorPower.map_apply_ιMulti_family, NumberField.mixedEmbedding.span_idealLatticeBasis, LinearMap.submoduleOf_span_singleton_of_mem, norm_orthogonalProjection_apply_le, Algebra.Extension.Hom.sub_one_tmul, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc_apply, mem_iSup_iff_exists_dfinsupp, FDRep.average_char_eq_finrank_invariants, isArtinian_range, TensorProduct.inner_mapIncl_mapIncl, RootPairing.toLinearMap_apply_PolarizationIn, exteriorPower.zeroEquiv_naturality, KaehlerDifferential.D_apply, TensorProduct.exists_finite_submodule_right_of_setFinite, HahnEmbedding.IsPartial.truncLT_mem_range, LinearIndependent.linearCombinationEquiv_apply_coe, Polynomial.adjSylvester_comp_sylveserMap, iSup_eq_range_dfinsupp_lsum, Module.Basis.span_apply, LinearMap.ker_codRestrict, CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, RootPairing.instFiniteSubtypeMemSubmoduleCorootSpanOfFinite, ContinuousLinearMap.equivRange_symm_apply, RootPairing.finrank_corootSpanIn, LinearIndependent.linearCombination_comp_repr, Ideal.quotientToQuotientRangePowQuotSucc_mk, coe_inclusion, instLocallyConvexSpaceSubtypeMemSubmodule, Polynomial.degreeLT.instFiniteSubtypeMemSubmodule, finrank_strictMono, Algebra.Extension.Cotangent.mk_eq_zero_iff, linearEquiv_det_reflection, LinearPMap.apply_comp_inclusion, LieSubmodule.toEnd_comp_subtype_mem, Matrix.rank_eq_finrank_range_toLin, Matrix.eRank_toNat_eq_finrank, CharacterModule.intSpanEquivQuotAddOrderOf_apply, Ideal.mapCotangent_toCotangent, stereoToFun_apply, prodEquivOfIsCompl_symm_apply_fst_eq_zero, exteriorPower.ιMulti_apply_coe, affineIndependent_iff_not_finrank_vectorSpan_le, coe_tensorSpanEquivSpan_apply_tmul, FG.lTensor.directLimit_apply', dualRestrict_def, ContinuousLinearMap.coe_projKerOfRightInverse_apply, Rep.coindToInd_apply, Module.Basis.SmithNormalForm.snf, AlgHom.toKerIsLocalization_apply, LinearMap.restrict_eq_codRestrict_domRestrict, IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite, HahnEmbedding.Partial.truncLT_mem_range_sSupFun, FG.rTensor.directLimit_apply, coe_continuous_linearProjOfClosedCompl, LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict, LieModule.Cohomology.d₁₂_apply_coe_apply_apply, coe_orthogonalDecomposition, rank_submodule_le_one_iff', finrank_orthogonal_span_singleton, inclusionSpan_apply_coe, comap_subtype_self, exteriorPower.oneEquiv_naturality, SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux, one_le_finrank_iff, IsPrincipal.generator_submoduleImage_dvd_of_mem, norm_subtypeL, RootPairing.posRootForm_posForm_pos_of_ne_zero, Module.Flat.eqLocus_lTensor_eq, LinearMap.lift_rank_eq_of_surjective, Subspace.dualRestrict_leftInverse, TensorProduct.exists_finite_submodule_left_of_finite, Module.instFiniteSubtypeMemIdealOfIsNoetherian, DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem_ne, rank_mono, LinearMap.comap_codRestrict, ContinuousLinearMap.coe_rangeRestrict, setLike.coe_galgebra_toFun, norm_sq_eq_add_norm_sq_projection, Polynomial.det_taylorLinearEquiv_toLinearMap, ContinuousLinearMap.equivRange_symm_toLinearEquiv, LinearEquiv.ofInjective_apply, comm_trans_rTensorOne, starProjection_apply, FractionalIdeal.isNoetherian_spanSingleton_inv_to_map_mul, linearIndependent_span, Subspace.flip_quotDualCoannihilatorToDual_bijective, comap_equiv_self_of_inj_of_le_apply, rank_quotient_add_rank_of_isDomain, Module.Basis.sumQuot_repr_inl_of_mem, exists_fg_le_subset_range_rTensor_subtype, DirectSum.coeAlgHom_of, TensorProduct.rTensor_injective_of_forall_vanishesTrivially, isArtinian_of_fg_of_artinian, set_smul_eq_map, RingHom.toKerIsLocalization_apply, Polynomial.degreeLT.addLinearEquiv_apply, fst_orthogonalDecomposition_apply, LinearEquiv.mem_dilatransvections_iff_finrank, Matrix.rank_eq_finrank_span_row, RootPairing.prod_rootForm_smul_coroot_mem_range_domRestrict, finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply, LinearEquiv.ofSubmodules_symm_apply, IsSemisimpleModule.exists_quotient_linearEquiv_submodule, LinearMap.kerComplementEquivRange_apply_coe, LinearDisjoint.rank_inf_le_one_of_commute_of_flat_right, restrictScalarsEquiv_symm_apply, LinearMap.quotientInfEquivSupQuotient_injective, isArtinian_of_submodule_of_artinian, Module.Basis.restrictScalars_repr_apply, CliffordAlgebra.GradedAlgebra.ι_apply, LieModule.Cohomology.d₁₂_apply_apply_ofTrivial, GradedTensorProduct.auxEquiv_mul, lTensorOne'_tmul, RootPairing.CoPolarizationIn_eq, rTensorOne'_tmul_one, inner_orthogonalProjection_eq_of_mem_right, DirectSum.decompose_symm_algebraMap, LinearMap.ker_domRestrict, rTensorOne'_tmul, Finsupp.linearCombinationOn_range, Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex, TensorProduct.exists_finite_submodule_right_of_setFinite', realPart_comp_subtype_selfAdjoint, projective_units, RootPairing.algebraMap_rootFormIn, map_subtype_embedding_eq, le_linearEquiv_of_le_sSup, LinearDisjoint.injective, ZLattice.module_free, LinearMap.mem_submoduleImage, dualCopairing_apply, LinearEquiv.toSpanNonzeroSingleton_apply, Module.Flat.instSubalgebraToSubmodule, ContinuousLinearMap.coe_linearMap_equivRange, LinearMap.BilinForm.nondegenerate_restrict_iff_disjoint_ker, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, ker_inclusion, AffineIndependent.finrank_vectorSpan_image_finset, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, FractionalIdeal.isNoetherian_zero, comap_subtype_eq_top, LinearIndependent.span_repr_eq, prodEquivOfIsCompl_symm_apply, injective_tensorToSpan, projective_of_isUnit, Module.Basis.restrictScalars_apply, exteriorPower.ιMultiDual_apply_ιMulti, natAbs_det_equiv, Module.Basis.mem_submodule_iff', map_subtype_span_singleton, LinearPMap.adjointDomainMkCLM_apply, Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, exteriorPower.pairingDual_ιMulti_ιMulti, mulRightMap_eq_mulMap_comp, isNoetherian_submodule', exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, rank_span_finset_le, Ideal.quotientToQuotientRangePowQuotSucc_surjective, MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, finrank_map_le, finrank_span_eq_card, prodComm_trans_prodEquivOfIsCompl, DirectSum.decompose_algebraMap, LinearMap.compLeftInverse_apply_of_bdd, RootPairing.zero_le_posForm, finrank_eq_zero, rTensorOne_tmul, ContinuousLinearEquiv.toSpanNonzeroSingleton_symm_apply, exists_fun_fin_finrank_span_eq, Ideal.instIsTorsionFreeSubtypeMemSubmodule, LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_left, Module.Finite.of_isComplemented_domain, Polynomial.degreeLT.addLinearEquiv_apply', affineIndependent_iff_le_finrank_vectorSpan, Subspace.quotAnnihilatorEquiv_apply, skewAdjointPart_comp_subtype_selfAdjoint, unitsToPic_apply, instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy, coe_mulMap_comp_eq, exteriorPower.oneEquiv_symm_apply, instModuleFinite_of_discrete_submodule, LinearMap.finrank_range_le, isIdempotentElemEquiv_apply_coe, TensorProduct.exists_finite_submodule_left_of_finite', LinearEquiv.submoduleMap_apply, ContinuousLinearEquiv.ofSubmodule'_apply, Module.Flat.iff_lTensor_injective, LieModule.Cohomology.mem_twoCocycle_iff, exteriorPower.map_comp_ιMulti, Ideal.basisSpanSingleton_apply, TensorProduct.quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk, orthogonalProjection_apply_eq_linearProjOfIsCompl, TensorProduct.tensorQuotientEquiv_apply_mk_tmul, TensorProduct.exists_finite_submodule_of_finite, MeasureTheory.condExpL2_indicator_of_measurable, derivationToSquareZeroEquivLift_symm_apply_apply_coe, GradedTensorProduct.mulHom_apply, MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictDegreeOfFinite, linearEquiv_of_sSup_eq_top, AddMonoidAlgebra.GradesBy.decompose_single, ContinuousMultilinearMap.codRestrict_apply_coe, coe_isComplEquivProj_apply, IsCompactOperator.restrict, prodEquivOfIsCompl_symm_apply_left, sndL_comp_coe_orthogonalDecomposition, RootPairing.PolarizationIn_apply, injective_subtype, linearProjOfIsCompl_isCompl_projection, quotientEquivOfIsCompl_apply_mk_coe, MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp, DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem, LinearMap.coe_domRestrict, Module.End.isNilpotent_restrict_maxGenEigenspace_sub_algebraMap, linearProjOfIsCompl_comp_subtype, rank_eq_zero, IsLattice.finrank_of_pi, Polynomial.degreeLT.addLinearEquiv_symm_apply_inl, coe_subtypeₗᵢ, Polynomial.degreeLT.addLinearEquiv_symm_apply_inr_basis, MvPolynomial.weightedHomogeneousComponent_directSum, groupHomology.π_comp_H1Iso_hom_apply, LinearMap.quotKerEquivRange_symm_apply_image, Finsupp.restrictDom_comp_subtype, Module.Finite.span_singleton, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, rTensor_mkQ, groupCohomology.map_id_comp_H0Iso_hom_apply, exteriorPower.pairingDual_apply_apply_eq_one, Module.Flat.tensorProduct_mapIncl_injective_of_left, imaginaryPart_comp_subtype_selfAdjoint, iSupIndep.linearEquiv_apply, ContinuousLinearEquiv.coord_toSpanNonzeroSingleton, HasRankNullity.rank_quotient_add_rank, Module.Flat.iff_lTensor_injectiveₛ, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc_apply, torsionBy.mk_ideal_smul, IsLattice.rank_of_pi, IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite, norm_orthogonalProjection_apply, toENat_rank_span_set, torsionBySet_torsionBySet_eq_top, rTensorOne_tmul_one, toLinearMap_prodEquivOfIsCompl_symm, PeriodPair.latticeBasis_one, diffToIdealOfQuotientCompEq_apply, finrank_eq_rank, ZLattice.covolume_eq_det_mul_measureReal, Subspace.finrank_add_finrank_dualCoannihilator_eq, Function.Exact.linearMap_rangeRestrict, Module.Finite.range, TensorProduct.forall_vanishesTrivially_iff_forall_rTensor_injective, LinearIndependent.linearCombinationEquiv_symm_apply, equivSubtypeMap_apply, Algebra.Extension.Hom.mapKer_apply_coe, isIdempotentElemEquiv_symm_apply_coe, Algebra.Extension.contangentEquiv_tmul, det_reflection, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, LinearMap.quotKerEquivRange_apply_mk, Algebra.Generators.cMulXSubOneCotangent_eq, rank_span_le, ContinuousLinearEquiv.toSpanNonzeroSingleton_coord, Ideal.toCotangent_apply, inner_orthogonalProjection_eq_of_mem_left, LieAlgebra.InvariantForm.restrict_orthogonal_nondegenerate, rank_submodule_eq_one_iff, Finsupp.supportedEquivFinsupp_symm_apply_coe_support_val, ZLattice.exists_forall_abs_repr_le_norm, linearMap_eq_iff_of_eq_span, CategoryTheory.ShortComplex.exact_iff_surjective_moduleCatToCycles, RootPairing.prod_rootFormIn_smul_coroot_mem_range_PolarizationIn, Ideal.toCotangent_eq_zero, exteriorPower.ιMulti_family_span_of_span, NumberField.fractionalIdeal_rank, toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl, mulRightMap_apply, LieHom.quotKerEquivRange_invFun, IsLattice.free, Module.injOn_dualMap_subtype_span_range_range, LieSubalgebra.coe_ofLe, Real.Convex.dimH_eq_finrank_vectorSpan, quotientEquivOfIsCompl_symm_apply, GradedTensorProduct.auxEquiv_tmul, Ideal.cotangentEquivIdeal_apply, exteriorPower.map_injective_field, Subspace.dualLift_of_mem, LinearEquiv.coe_ofEq_apply, Polynomial.degreeLT.addLinearEquiv_symm_apply, coord_norm', RootPairing.algebraMap_posRootForm_posForm, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, Basis.mem_ideal_iff', Ideal.quotientToQuotientRangePowQuotSucc_injective, Algebra.idealMap_isLocalizedModule, DirectSum.decomposeLinearEquiv_apply, exteriorPower.alternatingMapLinearEquiv_comp, collinear_iff_rank_le_one, Finsupp.linearCombination_restrict, LinearEquiv.ofSubmodule'_toLinearMap, finrank_top, DirectSum.decomposeLinearEquiv_symm_comp_lof, exteriorPower.basis_coord, LinearIndependent.repr_range, Algebra.Extension.Cotangent.mk_eq_mk_iff_sub_mem, IsSemisimpleModule.exists_end_ringEquiv, Module.isPrincipal_submodule_iff, Ideal.constr_basisSpanSingleton, Function.Exact.iff_linearMap_rangeRestrict, RootPairing.range_polarizationIn, mulMap_one_left_eq, LinearMap.finrank_maxGenEigenspace, groupCohomology.coboundariesToCocycles₂_apply, MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite, quotDualCoannihilatorToDual_injective, MultilinearMap.codRestrict_apply_coe, TensorProduct.exists_finite_submodule_of_setFinite', MvPolynomial.DirectSum.coeLinearMap_eq_finsum, Subspace.dualRestrict_surjective, LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal', ker_subtypeL, LinearMap.kerComplementEquivRange_symm_apply, LinearMap.lift_rank_range_add_rank_ker, mulMap_comm_of_commute, TensorAlgebra.GradedAlgebra.ι_apply, MeasureTheory.integrable_condExpL2_of_isFiniteMeasure, PeriodPair.latticeEquiv_symm_apply, HahnEmbedding.ArchimedeanStrata.isInternal_stratum', exteriorPower.instFinite, LinearEquiv.coord_self, exteriorPower.alternatingMapToDual_apply_ιMulti, isArtinian_submodule', KaehlerDifferential.D_tensorProductTo, LinearEquiv.ofEq_symm, IsSemisimpleModule.exists_end_algEquiv, mulMap_eq_mul'_comp_mapIncl, DirectSum.decomposeLinearEquiv_symm_apply, LinearEquiv.ofLeftInverse_apply, setBasisOfTopLeSpanOfCardEqFinrank_repr_apply, liftOfDerivationToSquareZero_apply, Algebra.Extension.Cotangent.mk_surjective, rank_add_le_rank_add_rank, RootPairing.RootPositiveForm.isSymm_posForm, FractionalIdeal.isNoetherian_iff, mem_smul_top_iff, DirectSum.decomposeAlgEquiv_apply, AffineIndependent.finrank_vectorSpan, AddMonoidAlgebra.grade.decompose_single, IsCompl.projection_apply, LinearMap.comp_codRestrict, mulLeftMap_eq_mulMap_comp, Representation.subrepresentation_apply, MeasureTheory.integrable_condExpL2_indicator, rank_quotient_add_rank_le, LieAlgebra.Extension.d₁₂_oneCochainOfTwoSplitting, LinearMap.finrank_range_dualMap_eq_finrank_range, Algebra.Extension.Hom.subToKer_apply_coe, HahnEmbedding.ArchimedeanStrata.iSupIndep_stratum', LinearMap.IsProj.eq_conj_prod_map', LinearEquiv.submoduleMap_symm_apply, LinearMap.map_codRestrict, ZLattice.abs_repr_lt_of_norm_lt, LinearMap.BilinForm.finrank_orthogonal, Rep.coindVEquiv_apply_hom, DirectSum.IsInternal.card_filter_subordinateOrthonormalBasisIndex_eq, ContinuousMultilinearMap.codRestrict_toMultilinearMap, Polynomial.degreeLT.addLinearEquiv_symm_apply', LinearDisjoint.rank_le_one_of_flat_of_self, ContinuousLinearMap.projKerOfRightInverse_comp_inv, LinearEquiv.toSpanNonzeroSingleton_symm_apply_smul, Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_is_extension, instInvertibleSubtypeMemVal, AffineSubspace.linear_equivMapOfInjective, MeasureTheory.MemLp.condExpL2_ae_eq_condExp', LinearMap.BilinForm.IsSymm.restrict, toIsOrderedCancelAddMonoid, Ideal.rank_pow_quot_aux, isNoetherian_of_fg_of_noetherian, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_apply, Subspace.dualEquivDual_def, TensorProduct.quotientTensorEquiv_apply_tmul_mk, exists_finset_span_eq_linearIndepOn, exteriorPower.zeroEquiv_ιMulti, LinearMap.surjective_comp_linearProjOfIsCompl, LinearMap.exact_subtype_ker_map, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, Polynomial.eval_eq_sum_degreeLTEquiv, mulMap'_surjective, subtypeL_apply, finrank_span_eq_finrank_span, Subspace.dualLift_rightInverse, Ideal.natAbs_det_equiv, finrank_map_subtype_eq, ker_orthogonalProjection, LinearMap.ofIsCompl_add, LinearEquiv.ofSubmodule'_apply, FG.directedSystem, exteriorPower.map_injective, Ideal.rank_pow_quot, Ideal.subtype_isoBaseOfIsPrincipal_eq_mul, LinearDisjoint.rank_le_one_of_commute_of_flat_of_self, exteriorPower.basis_repr_apply, LinearIndependent.repr_eq, mk_quotientEquivOfIsCompl_apply, MvPolynomial.weightedDecomposition.decompose'_eq, prodEquivOfIsCompl_symm_apply_right, coe_mapIic_apply, submoduleOf_eq_top, Subspace.dualCopairing_nondegenerate, restrictScalars.isScalarTower, ContinuousLinearEquiv.submoduleMap_symm_apply, NumberField.mem_span_basisOfFractionalIdeal, Basis.mem_ideal_iff, LinearEquiv.ofTop_symm_apply, rank_span_of_finset, finrank_mono, mulLeftMap_apply_single, ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl, LinearIndependent.repr_ker, finrank_add_le_finrank_add_finrank, mulMap_map_comp_eq, Module.Flat.iff_lift_lsmul_comp_subtype_injective, Ideal.range_finsuppTotal, Module.Finite.top, IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite, finrank_le_one_iff_isPrincipal, Module.End.isNilpotent_restrict_sub_algebraMap, FG.lTensor.directLimit_apply, finrank_span_eq_finrank, LinearMap.IsProj.codRestrict_ker, Collinear.finrank_le_one, Module.fgSystem.equiv_comp_of, HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented_apply, RootPairing.posRootForm_posForm_nondegenerate, range_inclusion, Module.Flat.instSubtypeMemSubmoduleSubmoduleAlgebra, ContinuousLinearMap.projKerOfRightInverse_apply_idem, LinearMap.domRestrict₂_apply, Ideal.powQuotSuccInclusion_injective, LinearMap.IsProj.trace, IsLocalRing.CotangentSpace.map_eq_top_iff, rank_range_of_injective, HahnEmbedding.ArchimedeanStrata.archimedean_stratum, basisOfPid_bot, ContinuousLinearMap.coe_codRestrict_apply, LinearMap.restrict_smul_one, LinearMap.range_domRestrict, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end, instIsTorsionFree, coe_subtype, mulMap_comp_lTensor, LinearEquiv.rank_map_eq, isNoetherian_span_of_finite, RootPairing.algebraMap_coroot'In_apply, ContinuousLinearMap.IsPositive.orthogonalProjection_comp, LinearMap.linearEquiv_of_ne_zero, LinearMap.IsSymm.nondegenerate_restrict_of_isCompl_ker, dimH_orthogonalProjection_le, LinearMap.range_ofIsCompl, RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic, derivationOfSectionOfKerSqZero_apply_coe, torsionBy_isTorsionBy, Module.Finite.iff_fg, lTensorOne_symm_apply, LinearMap.tensorEqLocus_tmul, exteriorPower.map_comp_ιMulti_family, fg_top, RootPairing.rootFormIn_self_smul_coroot, tensorToSpan_apply_tmul, exteriorPower.map_id, LinearMap.ofIsCompl_left_apply, isCompl_comap_subtype_of_isCompl_of_le, Module.Finite.of_fg, iSupIndep_iff_dfinsupp_lsum_injective, Finsupp.supportedEquivFinsupp_symm_apply_coe, LinearEquiv.toSpanNonzeroSingleton_one, lTensorOne'_one_tmul, LinearMap.compAlternatingMap_codRestrict, LinearMap.coe_quotientInfToSupQuotient, Subspace.dualLift_injective, Algebra.Generators.cotangentRestrict_mk, Polynomial.toMatrix_sylvesterMap, TensorProduct.exists_finite_submodule_right_of_finite, LinearMap.subtype_compMultilinearMap_codRestrict, Finsupp.supportedEquivFinsupp_apply_support_val, ContinuousLinearMap.exist_extension_of_finiteDimensional_range, groupCohomology.π_comp_H2Iso_hom_apply, MeasureTheory.hausdorffMeasure_orthogonalProjection_le, CliffordAlgebra.even.lift.aux_apply, finrank_add_finrank_orthogonal, map_subtype_top, exteriorPower.pairingDual_apply_apply_eq_one_zero, lipschitzWith_orthogonalProjection, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, exists_fg_le_subset_range_rTensor_inclusion, derivationToSquareZeroEquivLift_apply_coe_apply, span_span_coe_preimage, Representation.coind_apply, ContinuousLinearEquiv.submoduleMap_apply, FractionalIdeal.abs_det_basis_change, ClosedComplemented.exists_submodule_equiv_prod, Rep.invariantsFunctor_map_hom, Module.End.iInf_maxGenEigenspace_restrict_map_subtype_eq, finrank_span_singleton, liftOfDerivationToSquareZero_mk_apply', ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection, Module.Finite.map, rank_le_one_iff_isPrincipal, subalgebra_top_finrank_eq_submodule_top_finrank, stereographic_apply, MeasureTheory.inner_condExpL2_eq_inner_fun, finite_dualAnnihilator_iff, linearProjOfIsCompl_comp_bijective_of_exact, RootPairing.RootPositiveForm.algebraMap_apply_eq_form_iff, groupCohomology.π_comp_H1Iso_hom_apply, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, LinearMap.rTensor_range, Module.Basis.SmithNormalForm.repr_comp_embedding_eq_smul, TensorProduct.exists_finite_submodule_right_of_finite', IsLocalRing.CotangentSpace.span_image_eq_top_iff, AlternatingMap.codRestrict_apply_coe, LinearEquiv.coord_apply_smul, inf_iInf_maxGenEigenspace_of_forall_mapsTo, LinearMap.finrank_maxGenEigenspace_zero_eq, fstL_comp_coe_orthogonalDecomposition, RootPairing.finrank_corootSpan_eq, LinearMap.ofIsCompl_right_apply, Polynomial.sylvesterMap_apply_coe, Polynomial.degreeLT.addLinearEquiv_natAdd, EuclideanGeometry.orthogonalProjection_linear, ContinuousLinearEquiv.ofSubmodule'_symm_apply, inclusion_injective, mulMap_comp_map_inclusion, orthogonalProjection_orthogonal_apply_eq_zero, LinearMap.submoduleComap_surjective_of_surjective, exteriorPower.basis_repr, exists_extension_norm_eq, NumberField.Units.unitLattice_rank, finrank_le, groupHomology.π_comp_H2Iso_hom_apply, isArtinian_sup, lTensorOne_tmul, instIsSimpleModuleSubtypeMemSubmoduleValSetSetOfNonemptyLinearEquivId, Module.Flat.iff_rTensor_injectiveₛ, LinearDisjoint.val_mulMap_tmul, LinearMap.trace_restrict_eq_of_forall_mem, Module.Dual.finrank_ker_add_one_of_ne_zero, Module.Finite.bot, Algebra.Extension.Hom.sub_tmul, exteriorPower.alternatingMapLinearEquiv_symm_apply, ZLattice.normBound_spec, instFreeSubtypeMemIdealOfFiniteOfIsTorsionFree, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π_hom, LinearMap.exists_extend, isNoetherian_submodule_left, Ideal.bot_lt_annihilator_of_disjoint_nonZeroDivisors, affineIndependent_iff_finrank_vectorSpan_eq, orthogonalProjectionFn_eq, RootPairing.finrank_rootSpanIn, Ideal.cotangentEquivIdeal_symm_apply, Module.flat_iff, Polynomial.taylorLinearEquiv_symm, DirectSum.IsInternal.ofBijective_coeLinearMap_of_ne, exists_fg_le_eq_rTensor_subtype, FractionalIdeal.isNoetherian, NumberField.Units.logEmbeddingEquiv_apply, Polynomial.degreeLT.addLinearEquiv_symm_apply_inl_basis, iSup_eq_toSubmodule_range, TensorProduct.exists_finite_submodule_of_setFinite, TensorProduct.exists_finite_submodule_left_of_setFinite', RootPairing.RootPositiveForm.zero_lt_apply_root_root_iff, exteriorPower.map_apply_ιMulti, NumberField.basisOfFractionalIdeal_apply, ContinuousAlternatingMap.codRestrict_apply_coe, Module.Basis.ofZLatticeComap_repr_apply, LinearMap.finrank_eq_of_isPerfPair, LinearMap.ker_restrict, RootPairing.posRootForm_posForm_anisotropic, rank_quotient_add_rank_of_divisionRing, Module.End.isNilpotent_restrict_genEigenspace_top, groupHomology.boundariesToCycles₂_apply, Module.Finite.span_finset, Module.Finite.instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule_1, AddMonoidAlgebra.decomposeAux_single, map_range_rTensor_subtype_lid, isNoetherian_sup, ContinuousLinearEquiv.coord_norm', LinearEquiv.coe_ofTop_symm_apply, IsLattice.finite, LinearMap.injective_domRestrict_iff, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_H, fstEquiv_symm_apply_coe, snd_orthogonalDecomposition_apply, LinearMap.BilinForm.toLin_restrict_ker_eq_inf_orthogonal, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_apply, Module.Basis.ofZLatticeBasis_repr_apply, fromModuleCatToModuleCatLinearEquiv_apply, Module.Finite.span_of_finite, IsIsotypic.linearEquiv_finsupp, fromModuleCatToModuleCatLinearEquiv_symm_apply_coe, LinearMap.surjective_rangeRestrict, linearProjOfIsCompl_range, NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, CharacterModule.intSpanEquivQuotAddOrderOf_apply_self, LinearMap.restrict_coe_apply, LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra, AlgHom.toKerIsLocalization_isLocalizedModule, FractionalIdeal.equivNum_apply, AddSubgroup.relIndex_eq_natAbs_det, isNoetherian_of_submodule_of_noetherian, orthogonalDecomposition_apply, map_comap_subtype, span_range_subtype_eq_top_iff, spanRank_top, exteriorPower.map_comp, Module.End.isNilpotent.restrict, groupHomology.π_comp_H1Iso_inv_apply, lift_rank_range_le, LinearMap.quotientInfEquivSupQuotient_symm_apply_left, exteriorPower.ιMultiDual_apply_nondiag, LinearMap.codRestrict_apply, AddMonoidAlgebra.decomposeAux_eq_decompose, mulMap_op, LinearEquiv.ofEq_rfl, torsionBySet.mk_smul, isNoetherian_top_iff, LieModule.Cohomology.mem_twoCocycle_iff_of_trivial, MeasureTheory.eLpNorm_condExpL2_le, finrank_vectorSpan_range_add_one_le, Module.Flat.tensorProduct_mapIncl_injective_of_right, ContinuousLinearEquiv.toSpanNonzeroSingleton_apply_coe, mem_span_set_iff_exists_finsupp_le_finrank, ContinuousLinearEquiv.coord_self, LinearMap.ofIsCompl_subtype_zero_eq, Derivation.liftKaehlerDifferential_apply, LinearEquiv.finrank_map_eq, map_subtype_range_inclusion, finrank_bot, ContinuousLinearEquiv.coord_norm, exteriorPower.map_surjective, KaehlerDifferential.DLinearMap_apply, LinearPMap.mem_adjoint_domain_iff, Module.Basis.coe_mkFinCons, CliffordAlgebra.GradedAlgebra.lift_ι_eq, linearProjOfIsCompl_ker, LinearEquiv.lift_rank_map_eq, EuclideanGeometry.orthogonalProjection_apply, Module.Basis.extendOfIsLattice_apply, torsion_isTorsion, rank_span, norm_orthogonalProjection, EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection, Polynomial.degreeLT.basisProd_natAdd, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange, mem_set_smul, lTensorOne_one_tmul, LinearMap.finrank_maxGenEigenspace_eq, LinearMap.IsProj.codRestrict_apply, LinearMap.BilinForm.toLin_restrict_range_dualCoannihilator_eq_orthogonal, LinearMap.nondegenerate_restrict_of_disjoint_orthogonal, rank_le_of_isSMulRegular, LinearPMap.coe_vadd, Module.Dual.eq_of_preReflection_mapsTo', finrank_lt, rank_sup_add_rank_inf_eq, MeasureTheory.condExpIndSMul_ae_eq_smul, rank_top, Module.fgSystem.instDirectedSystemSubtypeSubmoduleFGMemValCoeLinearMapId, isNoetherian_range, linearProjOfIsCompl_apply_eq_zero_iff, coplanar_iff_finrank_le_two, LinearMap.tensorKerEquiv_apply, finite_sup, LinearMap.range_codRestrict, mem_biSup_iff_exists_dfinsupp, exteriorPower.ιMulti_family_linearIndependent_ofBasis, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe, range_subtype, NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype, subtype_injective, dualRestrict_apply, LinearMap.BilinForm.finrank_add_finrank_orthogonal, Module.Basis.SmithNormalForm.toMatrix_restrict_eq_toMatrix, finrank_quotient, comapSubtypeEquivOfLe_apply_coe, RootPairing.RootPositiveForm.algebraMap_posForm, LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left, DirectSum.isInternal_biSup_submodule_of_iSupIndep, LinearMap.ker_le_range_iff, Ideal.map_toCotangent_ker, LinearMap.ofIsCompl_zero, exteriorPower.ιMulti_family_span, Polynomial.degreeLTEquiv_eq_zero_iff_eq_zero, toLocalized'_apply_coe, orthogonalProjection_comp_subtypeL_eq_zero_iff, dualQuotEquivDualAnnihilator_symm_apply_mk, LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate, Ideal.quotTorsionOfEquivSpanSingleton_apply_mk, Ideal.quotientToQuotientRangePowQuotSuccAux_mk, Module.Basis.sumQuot_inl, ZLattice.sum_piFinset_Icc_rpow_le, LinearEquiv.ofInjective_symm_apply, LieAlgebra.Extension.twoCocycleOf_coe_coe, ExteriorAlgebra.GradedAlgebra.ι_apply, Algebra.SubmersivePresentation.basisCotangent_apply, linearProjOfIsCompl_surjective, LinearMap.exists_extend_of_notMem, RootPairing.posRootForm_rootFormIn_posDef, HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun, LinearMap.comp_ker_subtype, mulMap_range, TensorProduct.tensorQuotientEquiv_symm_apply_tmul_mk, Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply, exteriorPower.oneEquiv_ιMulti, Algebra.Extension.Cotangent.map_mk, RootPairing.CoPolarizationIn_apply, orthogonalProjection_eq_zero_iff, CliffordAlgebra.GradedAlgebra.ι_sq_scalar, Polynomial.sylveserMap_comp_adjSylvester, exteriorPower.ιMulti_span, map_equivMapOfInjective_symm_apply, Finsupp.supportedEquivFinsupp_symm_apply_coe_apply, orthogonalProjection_starProjection_of_le, Real.exists_extension_norm_eq, LinearMap.finrank_range_add_finrank_ker, exteriorPower.toTensorPower_apply_ιMulti, coe_orthogonalProjection_apply, torsion'_torsion'_eq_top, instModuleFree_of_discrete_submodule, Representation.linHom.invariantsEquivRepHom_apply_hom, Ideal.natAbs_det_basis_change, Module.Flat.iff_rTensor_injective', skewAdjointPart_comp_subtype_skewAdjoint, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, Polynomial.degreeLT.basisProd_castAdd, finrank_add_eq_of_isCompl, Finsupp.supportedEquivFinsupp_apply_apply, FG.rTensor.directLimit_apply', LinearMap.restrict_eq_domRestrict_codRestrict, LieModule.Cohomology.d₂₃_comp_d₁₂, Subspace.quotDualCoannihilatorToDual_bijective, Ideal.toCotangent_surjective, lTensor_mkQ, norm_subtypeL_le, ContinuousLinearEquiv.fst_equivOfRightInverse, LinearMap.quotientInfEquivSupQuotient_symm_apply_right, exteriorPower.zeroEquiv_symm_apply, finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply, basis_of_pid_aux, torsion'_isTorsion', HahnEmbedding.Partial.apply_of_mem_stratum, sndEquiv_apply, RingHom.toKerIsLocalization_isLocalizedModule, LinearPMap.adjointAux_inner, sndEquiv_symm_apply_coe, Algebra.idealMap_apply_coe, comapSubtypeEquivOfLe_symm_apply, Module.End.genEigenspace_restrict, Matrix.rank_eq_finrank_span_cols, coe_subtypeL, orthogonalProjection_coe_eq_linearProjOfIsCompl, quotient_prod_linearEquiv, LinearMap.domRestrict₁₂_apply, Ideal.map_includeLeft_eq, orthogonalProjection_norm_le, ContinuousLinearEquiv.equivOfRightInverse_symm_apply, LinearMap.injective_rangeRestrict_iff, LinearDisjoint.rank_inf_le_one_of_flat_right, LinearMap.quotientInfEquivSupQuotient_surjective, LinearPMap.graph_map_snd_eq_range, ModuleCat.toKernelSubobject_arrow, orthogonalProjection_orthogonal, LinearMap.finrank_eigenspace_le, Module.Basis.SmithNormalForm.coord_apply_embedding_eq_smul_coord, LinearMap.domRestrict_apply, LinearMap.surjective_comp_subtype_of_isComplemented, Polynomial.taylorLinearEquiv_apply_coe, MeasureTheory.norm_condExpL2_le_one, Module.finrank_quotient_add_finrank_le, Module.Flat.iff_lTensor_injective', Module.Basis.addSubgroupOfClosure_apply, MeasureTheory.condExpL2_comp_continuousLinearMap, LinearEquiv.ofTop_apply, mulMap_comp_rTensor, Algebra.Extension.Cotangent.ker_mk, torsionBySet_isTorsionBySet, orthogonalProjection_orthogonalComplement_singleton_eq_zero, Polynomial.degreeLT.basis_repr, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end, Module.End.pos_finrank_genEigenspace_of_hasEigenvalue, LinearDisjoint.rank_inf_le_one_of_flat_left, orthogonalProjection_eq_linearProjOfIsCompl, LinearPMap.adjoint_apply_of_dense, RootPairing.range_polarizationIn_le_span_coroot, exists_smith_normal_form_of_le, MeasureTheory.condExpL2_const_inner, LinearPMap.toFun_eq_coe, map_subtype_le, coe_prodEquivOfClosedCompl, Module.Basis.restrictScalars_toMatrix, TensorProduct.exists_of_fg, torsionBy.mk_smul, Subalgebra.rank_toSubmodule, groupHomology.π_comp_H2Iso_inv_apply, LinearMap.BilinForm.restrict_apply, DirectSum.range_coeLinearMap, submoduleOf_self, Finsupp.range_restrictDom, LinearMap.BilinForm.nondegenerate_restrict_of_disjoint_orthogonal, linearIndepOn_iff_linearCombinationOnₛ, EuclideanGeometry.Sphere.finrank_orthRadius, ContinuousLinearEquiv.ofSubmodule'_toContinuousLinearMap, LinearMap.rank_range_add_rank_ker, finrank_vectorSpan_insert_le_set, coe_equivMapOfInjective_apply, disjoint_iff_comap_eq_bot, LinearMap.lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm, Subspace.finrank_add_finrank_dualAnnihilator_eq, TensorProduct.toLinearMap_mapInclIsometry, lsum_comp_mapRange_toSpanSingleton, RootPairing.algebraMap_root'In_apply, groupHomology.boundariesToCycles₁_apply, OrthogonalFamily.projection_directSum_coeAddHom, TensorProduct.range_mapIncl_mono, Module.Finite.of_isComplemented_codomain, MatrixModCat.fromMatrixLinear_apply_coe, PeriodPair.finrank_lattice, linearIndepOn_iff_linearCombinationOn, Module.Flat.instInvertibleSubtypeMemSubmoduleSubmoduleAlgebra, LinearMap.toKerIsLocalized_apply_coe, LinearMap.submoduleMap_surjective, LinearMap.finrank_le_of_isSMulRegular, LinearPMap.inverse_domain, exteriorPower.basis_repr_self, MeasureTheory.condExpL2_indicator_nonneg, flip_quotDualCoannihilatorToDual_injective, coe_prodEquivOfClosedCompl_symm, Module.Finite.instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule, Algebra.Extension.cotangentComplex_mk, mulRightMap_apply_single, Subspace.dualPairing_eq, subalgebra_top_rank_eq_submodule_top_rank, Int.submodule_toAddSubgroup_index_ne_zero_iff, fstEquiv_apply, Ideal.to_quotient_square_comp_toCotangent, retractionOfSectionOfKerSqZero_tmul_D, DirectSum.IsInternal.subordinateOrthonormalBasisIndex_def, finrank_vectorSpan_range_le, ContinuousLinearEquiv.ofSubmodules_apply, LinearMap.ofIsCompl_eq_add, span_range_inclusionSpan, LinearMap.surjective_domRestrict_iff, ZLattice.exists_finsetSum_norm_rpow_le_tsum, Subspace.dualEquivDual_apply, instIsLocalizedModuleSubtypeMemLocalized₀ToLocalized₀, Ideal.isoBaseOfIsPrincipal_apply, ZLattice.abs_repr_le, DirectSum.IsInternal.collectedBasis_repr_of_mem, MvPolynomial.decomposition.decompose'_eq, restrictScalarsEquiv_apply, ZLattice.covolume_eq_det, rank_range_of_surjective, LinearMap.restrict_apply, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply, natAbs_det_basis_change, nonempty_basis_of_pid, comap_subtype_le_iff, ContinuousLinearEquiv.ofSubmodules_symm_apply
copy 📖	CompOp	2 math math: coe_copy, copy_eq
inhabited 📖	CompOp	—
instPartialOrder 📖	CompOp	946 math math: comap_lt_comap_iff_of_surjective, IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal, isArtinian_iff, Ideal.quotientEquivAlgOfEq_coe_eq_factorₐ, MvPolynomial.vanishingIdeal_anti_mono, Polynomial.not_ker_le_map_C_of_surjective_of_quasiFiniteAt, toAddSubgroup_toZModSubmodule, toAddSubmonoid_toNatSubmodule, isNoetherian_iff', AffineSubspace.direction_inf, FG.rTensor.directedSystem, Ideal.comap_fiberIsoOfBijectiveResidueField_apply, disjoint_span_singleton', LinearMap.IsIdempotentElem.comp_eq_right_iff, LinearMap.ker_le_of_iterateMapComap_eq_succ, Ideal.span_le, Module.End.isSemisimple_restrict_iff, FiniteArchimedeanClass.ball_lt_closedBall, Ideal.comap_bot_le_of_injective, LinearMap.iterateRange_succ, Ideal.dvd_iff_le, MvPolynomial.radical_le_vanishingIdeal_zeroLocus, integralClosure_le_span_dualBasis, Ideal.subset_union, Valuation.leSubmodule_v_le_of_mem, Algebra.Extension.Cotangent.span_eq_top_of_span_eq_ker, LinearMap.map_le_map_iff, Valuation.ltIdeal_le_leIdeal, Valuation.supp_quot_supp, set_smul_le_iff, le_annihilator_iff, Subalgebra.toSubmodule_injective, Ideal.span_singleton_mul_le_span_singleton_mul, span_sInf_le, groupHomology.boundaries₂_le_cycles₂, IdealFilter.ringFilterBasis_sets, Polynomial.disjoint_ker_aeval_of_isCoprime, IsLocalization.AtPrime.coe_orderIsoOfPrime_apply_coe, IsFractionRing.coeSubmodule_strictMono, map_dualCoannihilator_le, Module.End.mem_invtSubmodule, LinearMap.injective_restrict_iff_disjoint, Ideal.mul_le_right, RingEquiv.idealComapOrderIso_apply, MonoidAlgebra.Submodule.exists_isCompl, ImplicitFunctionData.isCompl_ker, WithIdealFilter.mem_nhds_zero_iff, LieSubmodule.toSubmodule_le_toSubmodule, Ideal.le_span_singleton_mul_iff, LinearMap.le_ker_iff_comp_subtype_eq_zero, IdealFilter.isPFilter_gabrielComposition, PrimeSpectrum.equivSubtype_apply_coe, DividedPowers.IsDPMorphism.ideal_comp, AffineSubspace.direction_le, mulMap_one_right_eq, LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot, minimalPrimes_eq_minimals, Ring.isField_iff_isSimpleOrder_ideal, idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors, restrictScalars_monotone, Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, RootPairing.rootSpan_dualAnnihilator_le_ker_rootForm, ringKrullDim_eq_one_iff_of_isLocalRing_isDomain, Ideal.instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided, MvPolynomial.le_vanishingIdeal_zeroLocus, LinearMap.range_domRestrict_le_range, PrimeSpectrum.equivSubtype_symm_apply_asIdeal, Polynomial.degreeLT_mono, orthogonal_disjoint, PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical, Module.End.independent_genEigenspace, MvPolynomial.weightedHomogeneousSubmodule_mul, codisjoint_span_image_of_codisjoint, Valuation.leSubmodule_monotone, mul_one_div_le_one, Module.End.invtSubmodule.disjoint_mk_iff, LieModule.exists_genWeightSpace_zero_le_ker_of_isNoetherian, PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical, bot_lt_isotypicComponent, ValuationRing.le_total_ideal, RingHom.liftOfSurjective_comp, PrimeSpectrum.gc, exists_spanRank_le_and_le_height_of_le_height, PrimeSpectrum.vanishingIdeal_strict_anti_mono_iff, RootPairing.range_polarization_domRestrict_le_span_coroot, ContinuousLinearMap.ker_le_ker_iff_range_le_range, Ideal.subset_pointwise_smul_iff, Ideal.IsPrime.prod_le, Localization.localRingHom_mk', Ideal.bot_lt_of_maximal, ClosedComplemented.exists_isClosed_isCompl, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, UnitAddTorus.mFourierSubalgebra_coe, Module.mem_support_iff_of_finite, set_smul_mono_left, DividedPowers.SubDPIdeal.le_iff, LieSubalgebra.submodule_span_le_lieSpan, RootPairing.invtRootSubmodule.eq_top_iff, nilradical_le_prime, LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal, ValuationRing.TFAE, Module.Basis.flag_le_ker_dual, LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm, IsArtinian.eventuallyConst_of_isArtinian, le_linearEquiv_of_sSup_eq_top, FG.lTensor.directedSystem, Ideal.Filtration.smul_le, TwoSidedIdeal.instIsTwoSidedCoeOrderHomIdealAsIdeal, one_le_traceDual_one, comap_le_comap_smul, FractionalIdeal.coe_le_coe, exists_le_isAssociatedPrime_of_isNoetherianRing, map_span_le, IsSemisimpleModule.jacobson_le_annihilator, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_comap_ideal, Module.End.genEigenspace_directed, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, Subspace.dualAnnihilator_dualAnnihilator_eq, le_dualAnnihilator_dualCoannihilator, PrimeSpectrum.denseRange_comap_iff_minimalPrimes, iSup_map_single_le, Module.jacobson_lt_top, Ideal.map_under_le_under_map, RingHom.liftOfSurjective_comp_apply, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, one_mem_div, Module.End.maxGenEigenspace_eq, Subalgebra.mulMap_toLinearMap, Module.End.eigenspace_restrict_le_eigenspace, dualAnnihilator_map_dualMap_le, le_comap_range_lTensor, IsSimpleRing.tfae, Submonoid.adjoin_eq_span_of_eq_span, LieSubmodule.disjoint_toSubmodule, linearIndepOn_id_union_iff, TwoSidedIdeal.bot_asIdeal, IsLocalRing.maximalIdeal_le_jacobson, Ring.jacobson_smul_top_le, idealFactorsFunOfQuotHom_comp, Ring.DimensionLEOne.not_lt_lt, isSimpleModule_iff_isAtom, Module.End.maxGenEigenspace_eq_genEigenspace_finrank, Module.End.mapsTo_genEigenspace_of_comm, pow_smul_top_le, PrimeSpectrum.vanishingIdeal_anti_mono_iff, RootPairing.disjoint_corootSpan_ker_corootForm, IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe, IsIsotypic.submodule_linearEquiv_fun, Ideal.subset_union_prime', Ideal.jacobson_bot_polynomial_le_sInf_map_maximal, Ideal.quotientEquivAlgOfEq_coe_eq_factor, Representation.Coinvariants.le_comap_ker, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, le_div_iff_mul_le, Valuation.ltIdeal_v_le_of_mem, Ideal.toTwoSided_asIdeal, Finsupp.iInf_ker_lapply_le_bot, LieSubmodule.isCompl_toSubmodule, LinearMap.iInf_ker_proj_le_iSup_range_single, coe_isComplEquivProj_symm_apply, Ideal.le_radical, Ideal.Filtration.Stable.bounded_difference, LieSubalgebra.toSubmodule_le_toSubmodule, PreValuationRing.iff_ideal_total, LinearMap.map_le_map_iff', Ideal.comap_le_map_of_inverse, LieSubmodule.toSubmodule_orderEmbedding_apply, Algebra.span_le_adjoin, LinearMap.range_le_bot_iff, Ideal.factors_decreasing, span_le_of_C_coeff_mem, DividedPowers.SubDPIdeal.isSubideal, Module.mapEvalEquiv_apply, Module.Basis.flag_mono, IsLocalRing.exists_maximalIdeal_pow_le_of_finite_quotient, torsionBySet_le_torsionBySet_of_subset, span_smul_le, Ideal.pointwise_smul_subset_iff, Finsupp.span_le_supported_biUnion_support, LinearPMap.le_graph_iff, le_orthogonal_orthogonal, PrimeSpectrum.zeroLocus_subset_zeroLocus_iff, Ideal.instCovariantClassHSMulLe, Ideal.prod_le_inf, OrderIso.setIsotypicComponents_apply, LinearMap.isCompl_range_inl_inr, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, IsPrincipal.contentIdeal_le_span_iff_dvd, Subalgebra.mem_toSubmodule, rank_submodule_le_one_iff, Subalgebra.range_isScalarTower_toAlgHom, LinearMap.disjoint_inl_inr, prod_le_iff, Profinite.NobelingProof.GoodProducts.spanFin, Algebra.toSubmodule_bot, map_le_map_iff_of_injective, LinearIndependent.disjoint_span_image, nilradical_le_jacobson, RootPairing.exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule, LinearMap.span_preimage_le, AlgebraicGeometry.IsAffineOpen.ideal_le_iff, finite_span_isCompactElement, AddValuation.self_le_supp_comap, topologicalClosure_map, LieSubmodule.coe_map_toEnd_le, LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint, PowerSeries.map_constantCoeff_le_self_of_X_mem, Ideal.IsPrime.inf_le, AddSubmonoid.toNatSubmodule_toAddSubmonoid, Ideal.Quotient.factorₐ_refl, Ideal.map_le_comap_of_inv_on, LinearMap.bot_lt_ker_of_det_eq_zero, ProjectiveSpectrum.subset_zeroLocus_iff_le_vanishingIdeal, Ideal.IsPrime.inf_le', AddSubmonoid.toNatSubmodule_closure, Algebra.sInf_toSubmodule, LinearMap.isCompl_iSup_ker_pow_iInf_range_pow, groupCohomology.coboundaries₂_le_cocycles₂, Representation.invtSubmodule.coe_top, traceDual_top', Ideal.sup_pow_add_le_pow_sup_pow, AddSubgroup.toZModSubmodule_toAddSubgroup, Ideal.relNorm_le_comap, inf_genEigenspace, smul_le_self_of_tower, span_le_restrictScalars, instPosMulStrictMonoIdeal, linearIndependent_sum, Ideal.pow_succ_lt_pow, Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex, exists_le_ker_of_notMem, IsDedekindDomain.primesOverEquivPrimesOver_inertiagDeg_eq, height_strictMono, LinearMap.IsProj.isCompl, Ring.DimensionLeOne.prime_le_prime_iff_eq, strictMono_comap_prod_map, Module.End.map_genEigenrange_le, mem_annihilator', ValuationSubring.idealOfLE_le_of_le, Ideal.IsPrime.multiset_prod_map_le, le_traceDual_traceDual, Subalgebra.finrank_toSubmodule, PrimeSpectrum.sup_vanishingIdeal_le, TwoSidedIdeal.orderIsoIsTwoSided_symm_apply, restrictScalars_lt, IsNoetherian.wf, Finsupp.supported_comap_lmapDomain, Subalgebra.isIdempotentElem_toSubmodule, LinearMap.IsPerfectCompl.isCompl_right, Ideal.span_singleton_le_span_singleton, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, span_coeff_minpolyDiv, LieModule.exists_genWeightSpace_le_ker_of_isNoetherian, Module.Basis.addSubgroupOfClosure_repr_apply, toAddSubmonoid_strictMono, LinearMap.comap_leq_ker_subToSupQuotient, Ideal.le_of_dvd, Ideal.exists_le_prime_disjoint, disjoint_span_singleton, Ideal.disjoint_map_primeCompl_iff_comap_le, Module.End.invtSubmodule.isCompl_iff, Algebra.top_toSubmodule, one_le_one_div, Module.coe_length, Polynomial.map_under_lt_comap_of_weaklyQuasiFiniteAt, Ideal.homogeneousHull.gc, LinearMap.finrank_genEigenspace_le, codisjoint_iff_exists_add_eq, Module.Basis.isMaxChain_range_flag, LieModule.weight_vector_multiplication, Module.End.iSup_genEigenspace_eq, IsSimpleModule.isAtom, Ideal.comp_quotientMap_eq_of_comp_eq, Polynomial.gaussNorm_lt_one_iff_contentIdeal_le, Module.Basis.flag_le_ker_coord, iSup_dualAnnihilator_le_iInf, Module.End.genEigenspace_inf_le_add, CliffordAlgebra.range_ι_le_evenOdd_one, Module.End.eigenspace_le_genEigenspace, AddSubgroup.toIntSubmodule_symm, differentialIdeal_le_iff, HahnEmbedding.ArchimedeanStrata.disjoint_ball_stratum, singleton_span_isCompactElement, span_prod_le, LinearMap.disjoint_ker, DividedPowers.isDPMorphism_iff, restrictScalars_le, toAddSubgroup_mono, Module.length_eq_top_iff_infiniteDimensionalOrder, toSubalgebra_toSubmodule, IsDedekindDomain.primesOverEquivPrimesOver_apply, traceForm_dualSubmodule_adjoin, FractionalIdeal.adjoinIntegral_coe, CliffordAlgebra.one_le_evenOdd_zero, AlgebraicGeometry.Scheme.IdealSheafData.le_ofIdeals_iff, Subalgebra.mul_toSubmodule, LinearPMap.HasCore.le_domain, Algebra.adjoin_nonUnitalSubalgebra_eq_span, ArchimedeanClass.ball_le_closedBall, atom_iff_nonzero_span, instMulLeftMono, Ideal.le_pow_ramificationIdx, AlgebraicGeometry.AffineSpace.spec_le_iff, finrank_strictMono, LinearPMap.apply_comp_inclusion, LinearMap.ker_prod_ker_le_ker_coprod, mk_mem_projectivization_iff, Module.jacobson_pi_le, jacobson_smul_lt_top, Finsupp.codisjoint_supported_supported, LinearPMap.sSup_apply, map_strictMono_of_injective, isNoetherian_iff_fg_wellFounded, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, TensorAlgebra.ι_range_disjoint_one, isCoatom_comap_iff, FG.lTensor.directLimit_apply', FG.rTensor.directLimit_apply, PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal, LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict, IsLocalization.bot_lt_comap_prime, Ideal.pi_le_pi_iff, rank_submodule_le_one_iff', PrimeSpectrum.vanishingIdeal_anti_mono, ker_liftQ_eq_bot', orderIsoMapComap_apply', FractionalIdeal.isFractional_adjoin_integral, ExteriorAlgebra.ι_range_disjoint_one, Ideal.exists_radical_pow_le_of_fg, SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux, FractionalIdeal.coeIdeal_le_coeIdeal', mem_integralClosure_iff_mem_fg, Subrepresentation.submoduleSubrepresentationOrderIso_apply, nonzero_span_atom, smul_top_inf_eq_smul_of_isSMulRegular_on_quot, toIntSubmodule_toAddSubgroup, RingOfIntegers.not_dvd_exponent_iff, toAddSubmonoid_mono, TwoSidedIdeal.asIdeal_jacobson, le_topologicalClosure, IsArtinian.monotone_stabilizes, traceDual_le_span_map_traceDual, orthogonal_gc, Ideal.mul_le, mem_colon_iff_le, TwoSidedIdeal.mem_fromIdeal, Module.length_submodule, linearIndepOn_iff_disjoint, Subalgebra.adjoin_eq_span_basis, comap_strictMono_of_surjective, Module.mem_support_iff_exists_annihilator, ConvexCone.IsGenerating.top_le_span, LinearMap.annihilator_le_of_injective, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, Ring.KrullDimLE.mem_minimalPrimes_iff_le_of_isPrime, Finsupp.isCompl_range_lmapDomain_span, AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono, isOrtho_iff_le, disjoint_ker_of_finrank_le, Ideal.pow_le_self, MvPolynomial.restrictSupport_mono, TwoSidedIdeal.mem_asIdealOpposite, map_subtype_embedding_eq, Module.jacobson_le_of_eq_bot, Ideal.exists_le_prime_notMem_of_isIdempotentElem, Subalgebra.mul_toSubmodule_le, LinearMap.iterateKer_coe, le_comap_mkQ, Module.Flat.instSubalgebraToSubmodule, Module.End.disjoint_genEigenspace, LinearMap.BilinForm.nondegenerate_restrict_iff_disjoint_ker, IsDedekindDomain.primesOverEquivPrimesOver_ramificationIdx_eq, RootPairing.isCompl_rootSpan_ker_rootForm, Algebra.adjoin_toSubmodule_le, RootPairing.GeckConstruction.span_range_h_le_range_diagonal, comap_subtype_eq_top, inf_iSup_genEigenspace, IsLocalization.coeSubmodule_le_coeSubmodule, isCompl_orthogonal_of_hasOrthogonalProjection, Ideal.IsPrime.multiset_prod_le, RootPairing.invtRootSubmodule.eq_bot_iff, toAddSubgroup_toIntSubmodule, Ideal.setOf_isPrincipal_wellFoundedOn_gt, Profinite.NobelingProof.GoodProducts.span, MvPolynomial.le_coeffsIn_pow, Module.End.genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le, le_comap_map, instCovariantClassHSMulLe, Module.End.isFinitelySemisimple_iff, closure_le, set_has_minimal_iff_artinian, Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, vectorSpan_mono, Valuation.ltSubmodule_monotone, le_isotypicComponent, IsNoetherian.wellFoundedGT, differentialIdeal_le_fractionalIdeal_iff, Module.End.disjoint_iInf_maxGenEigenspace, WittVector.ker_map_le_ker_mk_comp_ghostComponent, Ideal.le_comap_of_ramificationIdx_ne_zero, Ideal.isSimpleOrder, AddSubgroup.toZModSubmodule_symm, Ideal.span_singleton_le_iff_mem, AlgHom.IsArithFrobAt.le_comap, Ring.jacobson_le_of_isMaximal, Ideal.le_spanNorm_spanNorm, Module.Basis.flag_covBy, Ideal.idealProdEquiv_symm_apply, Ideal.homogeneousHull_mono, toConvexCone_le_toConvexCone, orderIsoMapComap_symm_apply', orderIsoMapComapOfBijective_symm_apply, Module.End.mem_genEigenspace_top, InnerProductSpace.nullSubmodule_le_ker_toDualMap_left, RingEquiv.idealComapOrderIso_symm_apply, DirectSum.IsInternal.isCompl, Module.End.injOn_genEigenspace, Ideal.map_le_comap_of_inverse, MvPolynomial.le_zeroLocus_iff_le_vanishingIdeal, Module.End.genEigenspace_one, smul_le_right, Ideal.Filtration.antitone, Algebra.inf_toSubmodule, Ideal.IsRadical.radical_le_iff, AddSubmonoid.toNatSubmodule_symm, LinearMap.hasEigenvalue_zero_tfae, Ideal.comap_le_comap_iff_of_surjective, Algebra.adjoin_eq_span_of_subset, PointedCone.minTensorProduct_le_maxTensorProduct, Ideal.isCoprime_tfae, Ideal.map_radical_le, Ideal.quotEquivOfEq_eq_factor, IsAdicComplete.le_jacobson_bot, DividedPowers.IsSubDPIdeal.isSubideal, coe_isComplEquivProj_apply, Module.Basis.flag_lt_flag, Ideal.le_toIdeal_homogeneousHull, le_traceDual, Module.End.invtSubmodule.mk_eq_top_iff, Subalgebra.linearDisjoint_iff, Valuation.leIdeal_v_le_of_mem, IsFractionRing.coeSubmodule_le_coeSubmodule, goursatFst_prod_goursatSnd_le, IsSemisimpleModule.sSup_simples_le, comapMkQOrderEmbedding_eq, RingHom.liftOfRightInverse_comp_apply, PrimeSpectrum.exists_primeSpectrum_prod_le, Module.FaithfullyFlat.range_le_ker_of_exact_rTensor, Ideal.IsPrime.mul_le, map_le_isotypicComponent, le_span_singleton_iff, span_le_span_iff, EuclideanGeometry.Sphere.direction_orthRadius_le_iff, Subalgebra.map_toSubmodule, instCanonicallyOrderedAdd, DividedPowers.DPMorphism.ideal_comp, Ideal.pow_le_pow_right, orderIsoMapComap_symm_apply, Ideal.radical_eq_sInf, DividedPowers.isDPMorphism_def, IsSemisimpleModule.jacobson_le_ker, LinearMap.IsIdempotentElem.comp_eq_left_iff, Ideal.eq_jacobson_iff_notMem, le_traceDual_comm, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, span_lt_top_of_card_lt_finrank, span_range_natDegree_eq_adjoin, AddSubgroup.coe_toZModSubmodule, idealFactorsEquivOfQuotEquiv_symm, AffineSubspace.direction_iInf, Ideal.ker_le_comap, IsOrtho.le, AlgebraicClosure.le_maxIdeal, Finsupp.disjoint_supported_supported, IsPRadical.ker_le, disjoint_def', Ideal.map_le_iff_le_comap, IsMinimalPrimaryDecomposition.minimal, rank_submodule_eq_one_iff, Ideal.homogeneousCore'_le, LinearMap.range_prod_le, orderIsoMapComap_apply, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_descH_hom, Ideal.mem_normalizedFactors_iff, Polynomial.span_of_finite_le_degreeLT, IsIntegralClosure.range_le_span_dualBasis, Ideal.matrix_jacobson_le, toAddSubgroup_strictMono, Module.End.genEigenspace_eq_iSup_genEigenspace_nat, Ideal.Filtration.pow_smul_le_pow_smul, Module.Finite.instIsCoatomicSubmodule, Module.Basis.SmithNormalForm.le_ker_coord_of_notMem_range, top_le_span_range_iff_forall_exists_fun, map₂_le, Algebra.iInf_toSubmodule, isSimpleModule_iff, LinearMap.eventually_isCompl_ker_pow_range_pow, fourierSubalgebra_coe, Module.End.eventually_disjoint_ker_pow_range_pow, monotone_stabilizes_iff_noetherian, Polynomial.not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt, dualAnnihilator_gc, Profinite.NobelingProof.spanFinBasis.span, Subalgebra.finiteDimensional_toSubmodule, gc_map_comap, mem_projectivization_iff_submodule_le, instCovariantClassHSMulLe_1, sup_dualAnnihilator_le_inf, linearIndepOn_union_iff, Subalgebra.toSubmodule_toSubalgebra, inf_comap_le_comap_add, AddMonoidHom.coe_toIntLinearMap_ker, RingHom.pNilradical_le_ker_of_perfectRing, Algebra.adjoin_union_coe_submodule, Ideal.exists_maximal_not_isPrincipal, mulMap_one_left_eq, LinearMap.range_le_iff_comap, toAddSubmonoid_le, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, Ideal.span_singleton_mul_left_mono, Module.AEval.mem_mapSubmodule_symm_apply, Valuation.ltSubmodule_le_leSubmodule, Valuation.leIdeal_mono, LinearMap.disjoint_ker_iff_injOn, Module.Basis.flag_wcovBy, le_orthogonal_iff_le_orthogonal, AddSubgroup.coe_toIntSubmodule, ProjectiveSpectrum.gc_ideal, fg_adjoin_of_finite, Ring.jacobson_le_of_eq_bot, Module.End.genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex, AffineSubspace.direction_lt_of_nonempty, disjoint_span_singleton_of_notMem, ClosedSubmodule.toSubmodule_le_toSubmodule, Ideal.subset_union_prime_finite, Ideal.IsMaximal.out, RingHom.liftOfRightInverse_comp, Ideal.mul_le_left, Algebra.adjoin_eq_span, Ideal.IsPrime.pow_le_iff, ContinuousMap.ideal_gc, isCompl_iff_disjoint, Ideal.radical_le_radical_iff, ValuationRing.iff_ideal_total, CliffordAlgebra.even_toSubmodule, Module.End.genEigenspace_zero_nat, Algebra.toSubmodule_eq_top, Representation.le_comap_invariants, Algebra.Generators.disjoint_ker_toKaehler_of_linearIndependent, Finsupp.disjoint_lsingle_lsingle, TwoSidedIdeal.top_asIdeal, IsLocalization.orderIsoOfPrime_symm_apply_coe, TwoSidedIdeal.mem_asIdeal, SubmodulesRingBasis.leftMul, Module.End.mem_invtSubmodule_symm_iff_le_map, Finsupp.codisjoint_supported_supported_iff, CategoryTheory.ShortComplex.moduleCat_exact_iff_ker_sub_range, Module.End.genEigenspace_top, Module.End.invtSubmodule.isCompl_mk_iff, Ideal.asIdeal_toTwoSided, RingHom.IsIntegral.quotient, Ideal.decomposition_erase_inf, LieAlgebra.InvariantForm.orthogonal_isCompl_toSubmodule, Ideal.span_singleton_mul_right_mono, toSubMulAction_strictMono, LinearMap.map_le_range, Ideal.isCompactElement_top, Subalgebra.pi_toSubsemiring, AffineMap.restrict.linear_aux, RingFilterBasis.SubmodulesBasis.inter, Ring.KrullDimLE.mem_minimalPrimes_iff, Module.fgSystem.instIsDirectedOrderSubtypeSubmoduleFG, Ideal.Filtration.pow_smul_le, LinearMap.disjoint_ker_of_nondegenerate_restrict, Polynomial.sup_ker_aeval_le_ker_aeval_mul, Finsupp.supported_mono, SubmodulesRingBasis.inter, Ring.map_jacobson_le, LinearMap.range_comp_le_range, AffineSubspace.direction_affineSpan_pair_le_iff_exists_smul, Ideal.homogeneousCore'_eq_sSup, IsSemisimpleModule.isCoatomic_submodule, Module.End.invtSubmodule.codisjoint_iff, Valuation.ltSubmodule_v_le_of_mem, AddMonoidHom.coe_toIntLinearMap_map, Ideal.ne_top_iff_exists_maximal, torsion_gc, Ideal.FG.isNilpotent_iff_le_nilradical, AffineSubspace.direction_sInf, FG.directedSystem, IsLocalRing.le_maximalIdeal, span_lt_of_subset_of_card_lt_finrank, IsOrtho.disjoint, LinearMap.IsIdempotentElem.isCompl, idealFactorsEquivOfQuotEquiv_is_dvd_iso, map_lt_map_iff_of_injective, IsAssociatedPrime.annihilator_le, coe_mapIic_apply, submoduleOf_eq_top, ProjectiveSpectrum.ideal_le_vanishingIdeal_zeroLocus, AddMonoidHom.coe_toIntLinearMap_range, Subalgebra.coe_pi, instIsOrderedRing, exists_isCompl, span_mono, Module.End.eigenspace_le_maxGenEigenspace, Ideal.le_comap_map, ModuleCat.disjoint_span_sum, CliffordAlgebra.evenOdd_mul_le, Ideal.Filtration.mono, Module.End.generalized_eigenvec_disjoint_range_ker, le_div_iff, Module.Basis.flag_le_iff, Ideal.radical_le_jacobson, lt_sup_iff_notMem, Module.length_eq_coheight, FG.lTensor.directLimit_apply, Module.fgSystem.equiv_comp_of, PointedCone.dual_le_dual, Subrepresentation.subrepresentationSubmoduleOrderIso_symm_apply, RootPairing.coe_bot, comap_le_comap_iff_of_surjective, FractionalIdeal.instPosMulReflectLEIdealOfIsDedekindDomain, Ideal.comap_le_map_of_inv_on, Ideal.ringJacobson_le_jacobson, Module.End.mem_genEigenspace_one, smul_comap_le_comap_smul, MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection, Ideal.pointwise_smul_le_pointwise_smul_iff, Subspace.map_le_dualAnnihilator_dualAnnihilator, Ideal.radical_iInf_le, Ideal.le_comap_pow, AddMonoidHom.coe_toIntLinearMap_comap, Ideal.map_inf_le, AffineSubspace.sup_direction_le, Module.End.IsFinitelySemisimple.genEigenspace_eq_eigenspace, LinearMap.isCoatom_ker_of_surjective, idealFactorsFunOfQuotHom_id, LinearMap.BilinForm.le_orthogonal_orthogonal, Ideal.mul_le_inf, smul_le, instMulPosStrictMonoIdeal, LinearMap.ker_sup_ker_le_ker_comp_of_commute, instIsSimpleOrderIdeal, Module.Basis.flag_le_flag, Module.End.genEigenspace_div, Ideal.span_mono, mul_le, IsLocalRing.exists_maximalIdeal_pow_le_of_isArtinianRing_quotient, LinearMap.iterateRange_coe, le_orthogonalBilin_orthogonalBilin, Profinite.NobelingProof.GoodProducts.span_iff_products, le_isotypicComponent_iff, IsDedekindDomain.primesOverEquivPrimesOver_symm_apply, mk_le_mk, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mono, LinearMap.ker_le_iff, Module.End.genEigenspace_eq_genEigenspace_finrank_of_le, LinearMap.le_comap_isotypicComponent, Ideal.coe_piOrderIso_symm_apply, RootPairing.isIrreducible_iff_invtRootSubmodule, LieSubmodule.codisjoint_toSubmodule, Module.length_ne_top_iff_finiteDimensionalOrder, is_simple_module_of_finrank_eq_one, Module.Basis.flag_le_ker_coord_iff, eventuallyConst_of_isNoetherian, TwoSidedIdeal.gc, AddSubmonoid.coe_toNatSubmodule, Ideal.pow_right_strictAnti, Module.End.genEigenspace_nat, Ideal.spanNorm_le_comap, exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, Ideal.span_singleton_lt_span_singleton, LinearMap.map_span_le, Ideal.homogeneousCore'_mono, Ideal.matrix_strictMono_of_nonempty, Polynomial.map_under_lt_comap_of_quasiFiniteAt, Subalgebra.coe_toSubmodule, LinearMap.le_eqLocus, Ideal.exists_le_maximal, FG.jacobson_smul_lt, LinearMap.range_dualMap_le_dualAnnihilator_ker, bot_lt_isotypicComponents, fg_iff_compact, ContinuousLinearMap.ker_prod_ker_le_ker_coprod, AddSubgroup.toIntSubmodule_toAddSubgroup, Module.End.genEigenspace_le_maximal, monotone_stabilizes_iff_artinian, LinearMap.ker_le_ker_comp, RootPairing.coe_top, PrimeSpectrum.exist_mem_one_of_mem_maximal_ideal, Module.End.mem_genEigenspace_nat, le_comap_single_pi, FiniteArchimedeanClass.submodule_strictAnti, IsSimpleModule.toIsSimpleOrder, Subspace.dualAnnihilator_le_dualAnnihilator_iff, Module.Relations.Solution.span_relation_le_ker_π, Module.Baer.ExtensionOf.le, Module.End.isSemisimple_iff', Ideal.quotientMap_injective, wellFoundedGT, IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, mem_iSup_of_chain, Subalgebra.restrictScalars_toSubmodule, orderIsoMapComapOfBijective_apply, le_dualAnnihilator_iff_le_dualCoannihilator, Ideal.spanNorm_mul_spanNorm_le, Ideal.bot_lt_annihilator_of_disjoint_nonZeroDivisors, StarAlgebra.adjoin_eq_span, Polynomial.span_le_degreeLE_of_finite, AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le, IsOrtho.ge, Module.length_quotient, Module.length_eq_height, DividedPowers.SubDPIdeal.sup_carrier_def, iSup_eq_toSubmodule_range, Ideal.le_pow_of_le_ramificationIdx, isSimpleModule_iff_isCoatom, LinearMap.iSup_range_single_le_iInf_ker_proj, Ideal.pow_lt_self, Localization.le_comap_primeCompl_iff, Module.Basis.mem_toFlag, LinearPMap.le_graph_of_le, LinearMap.disjoint_single_single, LinearMap.eventually_codisjoint_ker_pow_range_pow, RootPairing.corootSpan_dualAnnihilator_le_ker_rootForm, Ideal.exists_comap_eq_of_mem_minimalPrimes, Ideal.subset_union_prime, idealFactorsFunOfQuotHom_coe_coe, orthogonal_le_orthogonal_iff, orthogonal_le_iff_orthogonal_le, span_singleton_le_iff_mem, map_comap_le, IsIntegral.fg_adjoin_singleton, LinearMap.isCompl_span_singleton_orthogonal, FiniteArchimedeanClass.ball_strictAnti, Ideal.multiset_prod_le_inf, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, torsionBy_le_torsionBy_of_dvd, TwoSidedIdeal.orderIsoIsTwoSided_apply_coe, TwoSidedIdeal.asIdeal_matrix, starProjection_le_starProjection_iff, IsSemisimpleModule.eq_bot_or_exists_simple_le, disjoint_def, Ideal.le_comap_sup, IsLocalization.coeSubmodule_strictMono, set_has_maximal_iff_noetherian, Module.End.ker_pow_le_ker_pow_finrank, span_preimage_le, groupCohomology.coboundaries₁_le_cocycles₁, Polynomial.contentIdeal_le_span_content, WithIdealFilter.mem_nhds_iff, range_ker_disjoint, le_traceDual_mul_iff, Ideal.homogeneousCore_eq_sSup, Finsupp.lsingle_range_le_ker_lapply, AddSubgroup.relIndex_eq_natAbs_det, MvPolynomial.range_mapAlgHom, PrimeSpectrum.asIdeal_lt_asIdeal, span_singleton_smul_le, IsArtinian.set_has_minimal, Ideal.comap_fiberIsoOfBijectiveResidueField_symm, LinearMap.isCompl_of_proj, Valuation.self_le_supp_comap, Module.Basis.toFlag_carrier, instIsAtomisticSubmodule, LinearMap.annihilator_le_of_surjective, Ideal.exists_spanRank_eq_and_height_eq, span_monotone, finset_span_isCompactElement, Ideal.homogeneousCore_mono, DividedPowers.SubDPIdeal.lt_iff, map_le_iff_le_comap, Module.map_jacobson_le, isSMulRegular_on_submodule_iff_disjoint_ker_lsmul_submodule, one_le, FiniteDimensional.subalgebra_toSubmodule, AddSubgroup.toIntSubmodule_closure, LinearMap.IsSymmetricProjection.le_iff_range_le_range, OrderIso.setIsotypicComponents_symm_apply, AddSubgroup.mem_toZModSubmodule, IsLocalRing.le_maximalIdeal_of_isPrime, HomogeneousIdeal.toIdeal_irrelevant_le, RootPairing.disjoint_rootSpan_ker_rootForm, Module.End.hasGenEigenvector_iff, Ideal.map_comap_le, Ideal.matrix_monotone, CharP.quotient_iff_le_ker_natCast, Module.End.mem_genEigenspace_zero, Valuation.ltIdeal_mono, restrictScalarsEmbedding_apply, Polynomial.contentIdeal_mul_le_mul_contentIdeal, Polynomial.degreeLE_mono, le_prod_iff, isPRadical_iff, MvPolynomial.homogeneousSubmodule_mul, Module.fgSystem.instDirectedSystemSubtypeSubmoduleFGMemValCoeLinearMapId, isIntegral_quotientMap_iff, IsLocalFrameOn.generating, Representation.invtSubmodule.coe_bot, LinearMap.disjoint_ker', IsLocalization.orderIsoOfPrime_apply_coe, Ideal.IsHomogeneous.radical_eq, Polynomial.contentIdeal_le_contentIdeal_of_dvd, Module.End.genEigenspace_le_genEigenspace_finrank, instIsOrderedAddMonoid, NumberField.mixedEmbedding.disjoint_span_commMap_ker, Ring.le_comap_jacobson, Ideal.span_prod_le, Module.End.mem_genEigenspace, Ideal.dvdNotUnit_iff_lt, Subalgebra.pointwise_smul_toSubmodule, instMulRightMono, groupHomology.boundaries₁_le_cycles₁, Ideal.Quotient.factor_eq, LinearMap.ker_le_range_iff, isSMulRegular_on_quot_iff_lsmul_comap_le, Ideal.isCoprime_iff_codisjoint, LinearMap.range_le_ker_iff, IdealFilter.isTorsionQuot_def, DividedPowers.dpow_span_isSubideal, IsPRadical.ker_le', Subalgebra.prod_toSubmodule, smul_top_le_comap_smul_top, Module.End.invtSubmodule.mk_eq_bot_iff, smul_le_span, Ideal.toIdeal_homogeneousCore_le, closedComplemented_iff_isClosed_exists_isClosed_isCompl, Ideal.IsPrime.radical_le_iff, RootPairing.isCompl_corootSpan_ker_corootForm, Ideal.le_comap_mul, Module.End.genEigenspace_zero, Finsupp.disjoint_supported_supported_iff, isFullyInvariant_iff_le_imp_isotypicComponent_le, map_add_le, LieSubmodule.submodule_span_le_lieSpan, covBy_span_singleton_sup, map_le_localized₀, LinearIndependent.isCompl_span_image, Ideal.homogeneousHull_eq_sInf, toAddSubgroup_le, Ideal.span_singleton_absNorm_le, LinearMap.le_ker_iff_map, wcovBy_span_singleton_sup, SubmodulesBasis.inter, Module.mem_support_iff_of_span_eq_top, IsLocalRing.finite_quotient_iff, Ideal.leadingCoeffNth_mono, decomposition_erase_inf, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, Module.End.mem_invtSubmodule_iff_map_le, Module.End.invtSubmodule.codisjoint_mk_iff, AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal, MvPolynomial.coeffsIn_le, Finsupp.lmapDomain_disjoint_ker, Module.Basis.isChain_range_flag, height_lt_top, FG.rTensor.directLimit_apply', CliffordAlgebra.evenOdd_isCompl, Module.End.genEigenspace_le_smul, IsLocalRing.local_hom_TFAE, isNoetherian_iff, HenselianRing.jac, Subrepresentation.subrepresentationSubmoduleOrderIso_apply, AlgHom.equalizer_toSubmodule, Ideal.coe_piOrderIso_apply, Polynomial.mul_contentIdeal_le_radical_contentIdeal_mul, set_smul_le, Module.AEval.mem_mapSubmodule_apply, Module.Basis.flag_strictMono, DirectSum.isInternal_submodule_iff_isCompl, Module.le_comap_jacobson, Subalgebra.pi_toSubmodule, AddValuation.supp_quot_supp, PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain, Module.End.genEigenspace_restrict, le_comap_range_rTensor, le_traceDual_iff_map_le_one, pNilradical_le_nilradical, ArchimedeanClass.ball_antitone, Ring.jacobson_lt_top, LieModule.range_traceForm_le_span_weight, lieModule_lcs_map_le, LinearMap.IsPerfectCompl.isCompl_left, Module.annihilator_le_of_mem_support, span_le, instCovariantClassSetHSMulLe, LinearMap.BilinForm.le_flip_dualSubmodule, LinearPMap.domain_mono, AffineSubspace.sup_direction_lt_of_nonempty_of_inter_empty, Module.Basis.addSubgroupOfClosure_apply, Module.End.invtSubmodule.disjoint_iff, Module.End.isSemisimple_iff, IsDedekindDomain.HeightOneSpectrum.ideal_ne_top_iff_exists, Module.End.pos_finrank_genEigenspace_of_hasEigenvalue, LinearMap.BilinForm.isCompl_orthogonal_of_restrict_nondegenerate, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, Ideal.le_jacobson, RootPairing.range_polarizationIn_le_span_coroot, Ideal.gc_map_comap, map_inf_le, PrimeSpectrum.le_vanishingIdeal_zeroLocus, map_subtype_le, le_dualCoannihilator_dualAnnihilator, Subalgebra.rank_toSubmodule, lt_top_of_finrank_lt_finrank, Subalgebra.fg_bot_toSubmodule, Projectivization.Subspace.mem_submodule_iff, TwoSidedIdeal.coe_asIdeal, LieModule.coe_lowerCentralSeries_ideal_le, disjoint_iff_comap_eq_bot, LinearMap.range_add_le, MvPolynomial.restrictTotalDegree_le_restrictDegree, Ideal.comap_jacobson, AlgebraicGeometry.Scheme.IdealSheafData.le_def, Ideal.instIsCoatomic, InnerProductSpace.nullSubmodule_le_ker_toDualMap_right, neg_le_neg, Ideal.comap_le_iff_le_map, IdealFilter.isUniform_iff_exists_ringFilterBasis, toSubMulAction_mono, Subrepresentation.submoduleSubrepresentationOrderIso_symm_apply, Ideal.map_eq_bot_iff_le_ker, Ideal.le_comap_pow_ramificationIdx, IsCoprime.codisjoint, Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top, coe_iSup_of_chain, Module.mapEvalEquiv_symm_apply, surjOn_iff_le_map, map_le_smul_top, Ideal.homogeneousCore.gc, Ideal.span_singleton_mul_le_iff, LinearMap.ker_le_comap, Ideal.le_colon, LinearMap.range_lt_top_of_det_eq_zero, LinearMap.comap_le_comap_iff, FractionalIdeal.coeIdeal_le_coeIdeal, LinearMap.BilinForm.isCompl_span_singleton_orthogonal, comap_subtype_le_iff, ZModModule.exists_submodule_subset_card_le, disjoint_span_singleton'', PrimeSpectrum.asIdeal_le_asIdeal, Polynomial.isIntegral_isLocalization_polynomial_quotient, neg_le, Ideal.isMaximal_def, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective
module' 📖	CompOp	48 math math: Ideal.selfBasis_def, derivationToSquareZeroOfLift_apply, Ideal.exists_smith_normal_form, injective_inclusionSpan, Ideal.powQuotSuccInclusion_apply_coe, isLocalizedModule, Algebra.Extension.Hom.sub_one_tmul, Ideal.quotientToQuotientRangePowQuotSucc_mk, AlgHom.toKerIsLocalization_apply, IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite, inclusionSpan_apply_coe, Module.instFiniteSubtypeMemIdealOfIsNoetherian, RingHom.toKerIsLocalization_apply, Ideal.quotientToQuotientRangePowQuotSucc_surjective, Ideal.instIsTorsionFreeSubtypeMemSubmodule, Ideal.basisSpanSingleton_apply, derivationToSquareZeroEquivLift_symm_apply_apply_coe, IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite, diffToIdealOfQuotientCompEq_apply, Algebra.Extension.Hom.mapKer_apply_coe, Ideal.cotangentEquivIdeal_apply, Basis.mem_ideal_iff', Ideal.quotientToQuotientRangePowQuotSucc_injective, Algebra.idealMap_isLocalizedModule, Ideal.constr_basisSpanSingleton, IsSemisimpleModule.exists_end_algEquiv, liftOfDerivationToSquareZero_apply, Algebra.Extension.Hom.subToKer_apply_coe, Ideal.rank_pow_quot_aux, Ideal.rank_pow_quot, Basis.mem_ideal_iff, Ideal.powQuotSuccInclusion_injective, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end, derivationOfSectionOfKerSqZero_apply_coe, derivationToSquareZeroEquivLift_apply_coe_apply, liftOfDerivationToSquareZero_mk_apply', Algebra.Extension.Hom.sub_tmul, instFreeSubtypeMemIdealOfFiniteOfIsTorsionFree, Ideal.cotangentEquivIdeal_symm_apply, Module.Finite.instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule_1, AlgHom.toKerIsLocalization_isLocalizedModule, finrank_quotient, toLocalized'_apply_coe, Ideal.quotientToQuotientRangePowQuotSuccAux_mk, RingHom.toKerIsLocalization_isLocalizedModule, Algebra.idealMap_apply_coe, Module.Finite.of_isComplemented_codomain, span_range_inclusionSpan
ofClass 📖	CompOp	1 math math: coe_ofClass
ofLinearComb 📖	CompOp	1 math math: coe_ofLinearComb
setLike 📖	CompOp	3078 math math: Ideal.mem_bot, IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal, exists_lieSubmodule_coe_eq_iff, TensorProduct.mapInclIsometry_apply, coe_sum, finrank_sup_add_finrank_inf_eq, Ideal.toCotangent_to_quotient_square, LinearMap.lTensor_ker_subtype_tensorKerEquiv_symm, instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe, KaehlerDifferential.kerCotangentToTensor_toCotangent, Rep.resCoindHomEquiv_symm_apply_hom, PrimeSpectrum.closure_range_comap, Rep.resCoindHomEquiv_apply_hom, groupCohomology.instEpiModuleCatH2π, HasStrictFDerivAt.map_implicitFunctionOfComplemented_eq, Polynomial.degreeLT.addLinearEquiv_symm_apply_inr, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, groupHomology.π_comp_H2Iso_hom_assoc, IsAdjoinRoot.repr_add_sub_repr_add_repr_mem_span, Rep.invariantsAdjunction_homEquiv_symm_apply_hom, LinearMap.eqOn_span', Affine.Simplex.altitudeFoot_restrict, TensorProduct.forall_vanishesTrivially_iff_forall_fg_rTensor_injective, LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, rTensorOne_symm_apply, LinearMap.IsProj.map_mem, mem_colon_span_singleton, topEquiv_symm_apply_coe, Ideal.Filtration.submodule_closure_single, Algebra.exists_unramified_of_isUnramifiedAt, iSupIndep.dfinsupp_lsum_injective, LinearMap.BilinForm.dualSubmoduleParing_spec, FG.rTensor.directedSystem, AffineSubspace.coe_vsub, quotientRel_def, disjoint_span_singleton', Algebra.idealMap_eq_ofEq_comp_toLocalized₀, Quotient.eq, continuousOn_stereoToFun, coe_continuous_linearProjOfClosedCompl', Ideal.span_le, groupHomology.mapCycles₂_comp_assoc, Module.End.isSemisimple_restrict_iff, ContinuousLinearMap.IsIdempotentElem.isClosed_range, Irreducible.maximalIdeal_eq_setOf_le_v_coe, RootPairing.posRootForm_posForm_apply_apply, Ideal.selfBasis_def, Ideal.Filtration.submodule_eq_span_le_iff_stable_ge, Module.Basis.mem_submodule_iff, LinearMap.BilinForm.dualSubmoduleToDual_apply_apply, coe_add, AlgebraicGeometry.Scheme.zeroLocus_iInf, supIndep_torsionBySet_ideal, OrthonormalBasis.orthogonalProjection_eq_sum, IsIsotypic.linearEquiv_fun, LinearPMap.mem_domain_sSup_iff, finrank_span_finset_eq_card, derivationToSquareZeroOfLift_apply, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_fst, finrank_span_set_eq_card, linearProjOfIsCompl_apply_left, Ideal.subset_union, groupCohomology.toCocycles_comp_isoCocycles₁_hom, ValuationSubring.valuation_lt_one_iff, subtype_comp_inclusion, Algebra.Extension.Cotangent.span_eq_top_of_span_eq_ker, MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum, IsSemisimpleModule.exists_submodule_linearEquiv_quotient, Module.mem_annihilator, Affine.Simplex.orthogonalProjectionSpan_map, EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, ExteriorAlgebra.GradedAlgebra.liftι_eq, groupCohomology.isoCocycles₁_hom_comp_i_apply, Ideal.pow_multiset_sum_mem_span_pow, isScalarTower, Module.support_quotient, PadicInt.lift_sub_val_mem_span, IsSemisimpleModule.submodule, smul_def, AffineMap.restrict.bijective, Finsupp.mem_supported_support, isConnected_compl_of_one_lt_codim, bot_coe, Polynomial.mem_image_comap_C_basicOpen, groupCohomology.mem_cocycles₂_def, mem_toAffineSubspace, RootPairing.root'In_corootSpanMem_eq_pairingIn, set_smul_le_iff, RootPairing.rootForm_restrict_nondegenerate_of_ordered, Polynomial.degreeLT.instFreeSubtypeMemSubmodule, algebraMap_mem, linearIndependent_option, span_subset_span, finrank_add_finrank_le_of_disjoint, ValuationSubring.image_maximalIdeal, tendsto_tsum_div_pow_atTop_integral, NumberField.canonicalEmbedding.mem_span_latticeBasis, orthogonalDecomposition_symm_apply, Ideal.finrank_eq_finrank, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, PeriodPair.hasSumLocallyUniformly_weierstrassP, vadd_def, Ideal.span_singleton_mul_le_span_singleton_mul, exteriorPower.basis_apply, Ideal.mem_span_iff_exists_isHomogeneous, LinearMap.IsProj.subtype_comp_codRestrict, NumberField.Units.logEmbedding_fundSystem, Ideal.exists_smith_normal_form, toIsOrderedAddMonoid, linearIndepOn_iff_notMem_span, mem_ideal_smul_span_iff_exists_sum, LinearMap.IsProj.codRestrict_apply_cod, RootPairing.instIsRootSystemSubtypeMemSubmoduleSpanRangeCoeEmbeddingRootCorootRestrictScalars', Finsupp.restrictDom_apply, span_span_of_tower, Valuation.mem_maximalIdeal_iff, rank_le_card_isVisible, exteriorPower.linearMap_ext_iff, PrimeSpectrum.localization_specComap_range, vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints, Ideal.toCotangent_eq, Ideal.subset_span, RootPairing.finrank_corootSpan_eq', mulMap_tmul, AddMonoidAlgebra.of'_mem_span, PeriodPair.coeff_weierstrassPExceptSeries, Valuation.mem_leSubmodule_iff, subsingleton_iff_eq_bot, comm_trans_lTensorOne, isNoetherian_submodule_right, Polynomial.toMatrix_sylvesterMap', Valuation.mem_supp_iff, IdealFilter.ringFilterBasis_sets, iUnion_ssubset_of_forall_ne_top_of_card_lt, exists_fg_le_eq_rTensor_inclusion, Ideal.mem_span_singleton', LinearMap.IsRefl.domRestrict, Ideal.mem_ofPolynomial, Affine.Simplex.finiteDimensional_direction_altitude, TensorProduct.range_mapIncl, LinearMap.BilinForm.ker_restrict_eq_of_codisjoint, IsIsotypic.isotypicComponents, toLinearEquiv_orthogonalDecomposition_symm, NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, IsAdjoinRoot.mem_ker_map, isInternal_prime_power_torsion_of_pid, IsLocalization.AtPrime.coe_orderIsoOfPrime_apply_coe, Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection, mem_localized', smoothSheafCommRing.nonunits_stalk, RootPairing.EmbeddedG2.mem_span_of_mem_allRoots, PeriodPair.derivWeierstrassPExcept_sub, mem_reesAlgebra_iff_support, Ideal.isHomogeneous_iff_subset_iInter, covBy_iff_quot_is_simple, lift_rank_map_le, PrimeSpectrum.zeroLocus_nilradical, MeasureTheory.norm_condExpL2_le, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_apply, Ideal.exists_mem_span_singleton_map_residueField_eq, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, instStrictConvexSpace, AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, tensorEquivSpan_apply_tmul, groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply, linearMap_eq_zero_iff_of_eq_span, MvPowerSeries.mem_hasEvalIdeal_iff, coe_mapAlgEquiv_symm_apply, PrimeSpectrum.zeroLocus_eq_univ_iff, Ideal.exists_nonzero_mem_of_ne_bot, StrongDual.polarSubmodule_eq_setOf, Algebra.Extension.H1Cotangent.equiv_apply, groupCohomology.cocyclesIso₀_hom_comp_f, PeriodPair.ω₁_div_two_notMem_lattice, Rep.resCoindAdjunction_counit_app_hom_hom, LinearMap.IsProj.mem_iff_map_id, Module.Basis.mem_span, Finsupp.supportedEquivFinsupp_symm_single, vsub_mem_vectorSpan, LinearDisjoint.not_linearIndependent_pair_of_flat_left, mem_sup', groupCohomology.H1π_comp_map_assoc, addSubgroupClass, Ideal.le_span_singleton_mul_iff, re_inner_starProjection_eq_normSq, mem_pairSelfAdjointMatricesSubmodule, groupHomology.mapCycles₁_comp_apply, DirectSum.decomposeAlgEquiv_symm_apply, Ring.coe_jacobson_quotient, Affine.Simplex.restrict_reindex, Ideal.mem_leadingCoeffNth_zero, finiteDimensional_vectorSpan_range, LinearMap.le_ker_iff_comp_subtype_eq_zero, MeasureTheory.inner_condExpL2_left_eq_right, LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, RootPairing.restrictScalars_coe_coroot, groupCohomology.π_comp_H0Iso_hom, addSubmonoidClass, Affine.Simplex.faceOppositeCentroid_restrict, GradedTensorProduct.tmul_zero_coe_mul_coe_tmul, linearProjOfIsCompl_apply_right, groupCohomology.π_comp_H1Iso_hom_assoc, prodEquivOfIsCompl_symm_apply_snd_eq_zero, exteriorPower.coe_basis, LinearMap.tensorKer_tmul, LinearMap.IsSymmetric.diagonalization_apply_self_apply, dense_iff_topologicalClosure_eq_top, ProjectiveSpectrum.zeroLocus_mul_ideal, finrank_vectorSpan_image_finset_le, EuclideanGeometry.orthogonalProjection_congr, Subspace.dualLift_of_subtype, mem_colon', mulMap_one_right_eq, LinearIndepOn.notMem_span, PadicInt.appr_spec, exteriorPower.ιMulti_family_linearIndependent_field, vsub_mem_vectorSpan_pair, ContinuousLinearEquiv.snd_equivOfRightInverse, AffineIsometryEquiv.ofTop_apply, span_setOf_mem_eq_top, IsLocalization.AtPrime.mk'_mem_maximal_iff, toLinearEquiv_orthogonalDecomposition, AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical, LinearPMap.mk_apply, MeasureTheory.condExpL2_ae_eq_zero_of_ae_eq_zero, Subspace.dualRestrict_comp_dualLift, Ideal.mem_colon_span_singleton, range_comap_of_surjective, groupCohomology.mapCocycles₂_comp_i, PrimeSpectrum.isRetrocompact_zeroLocus_compl_of_fg, LieSubalgebra.mem_map_submodule, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, dualQuotEquivDualAnnihilator_apply, ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm, Finsupp.instCountableSubtypeMemSubmoduleSpanRange, coe_toAddSubmonoid, LinearIndependent.linearCombination_repr, exteriorPower.basis_repr_ne, IsLocalizedModule.exists_subsingleton_away, orthogonalProjection_mem_subspace_eq_self, LinearMap.range_domRestrict_le_range, RootPairing.Base.root_mem_span_int, RingPreordering.coe_support, MvPolynomial.homogeneousComponent_mem, ContinuousLinearMap.completeSpace_eqLocus, DirectSum.isInternal_ne_bot_iff, Module.isTorsionBySet_quotient_ideal_smul, Ideal.isHomogeneous_iff_forall_subset, Module.Basis.mk_repr, Valuation.mem_ltIdeal_iff, LinearMap.submoduleComap_apply_coe, finiteDimensional_direction_affineSpan_of_finite, Module.Flat.ker_lTensor_eq, KaehlerDifferential.cotangentComplexBaseChange_tmul, Module.Basis.ofZLatticeBasis_apply, DividedPowers.OfInvertibleFactorial.dpow_apply, Ideal.mem_pointwise_smul_iff_inv_smul_mem, groupCohomology.H0IsoOfIsTrivial_hom, PadicInt.sub_zmodRepr_mem, LinearMap.ofIsCompl_smul, OrthonormalBasis.orthogonalProjection_eq_sum_rankOne, mem_orthogonal_singleton_iff_inner_right, NumberField.mixedEmbedding.mem_idealLattice, BoxIntegral.unitPartition.mem_smul_span_iff, quotDualCoannihilatorToDual_apply, OrthogonalFamily.of_pairwise, injective_inclusionSpan, ContinuousMap.notMem_idealOfSet, IsLattice.rank', Span.repr_def, LinearMap.mem_isPairSelfAdjointSubmodule, bot_lt_isotypicComponent, dualPairing_apply, starProjection_singleton, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i_hom, mem_iSup_iff_exists_finsupp, AlgebraicGeometry.Scheme.zeroLocus_mul, LinearMap.tensorEqLocusEquiv_apply, PrimeSpectrum.gc, groupCohomology.coe_mapCocycles₁, LinearMap.domRestrict'_apply, groupHomology.mem_cycles₂_iff, Subrepresentation.mem_ofSubmodule'_iff, Fintype.mem_span_image_iff_exists_fun, Affine.Simplex.restrict_map_restrict, Valuation.Integers.isPrincipal_iff_exists_isGreatest, EuclideanGeometry.orthogonalProjection_contLinear, RootPairing.range_polarization_domRestrict_le_span_coroot, isUnit_iff_notMem_of_isAdicComplete_maximal, RootPairing.finrank_range_polarization_eq_finrank_span_coroot, EuclideanGeometry.dist_orthogonalProjection_eq_iff_oangle_eq, Module.FinitePresentation.exists_notMem_bijective, groupHomology.cyclesMap_comp_isoCycles₂_hom, mem_smul_span_singleton, ClosedComplemented.exists_isClosed_isCompl, range_specComap_of_surjective, ModuleCat.instSmallSubtypeForallCarrierObjMemSubmoduleSectionsSubmodule, Algebra.IsSmoothAt.exists_notMem_isStandardSmooth, AffineSubspace.coe_subtypeA, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces, RootPairing.invtRootSubmodule.eq_top_iff, finrank_vectorSpan_le_iff_not_affineIndependent, groupCohomology.coboundariesToCocycles₁_apply, groupHomology.mapCycles₁_comp_assoc, eq_top_iff', mem_span_image_iff_exists_fun, mem_iInf, LinearMap.BilinForm.restrict_nondegenerate_iff_isCompl_orthogonal, PeriodPair.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, PeriodPair.weierstrassP_coe, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, Ideal.notMem_of_isUnit, AffineSubspace.subtype_apply, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, Module.Basis.ofZLatticeComap_apply, le_linearEquiv_of_sSup_eq_top, FG.lTensor.directedSystem, IsLocalization.mem_span_map, Ideal.mem_toTwoSided, Ideal.ne_top_iff_one, rank_map_le, subtypeₗᵢ_toContinuousLinearMap, LinearMap.tensorKer_coe, LinearMap.BilinForm.restrict_nondegenerate_orthogonal_spanSingleton, finrank_quotient_add_finrank, isIsotypicOfType_submodule_iff, map_span_le, closure_subset_topologicalClosure_span, val_mulMap'_tmul, Finsupp.mem_supported, isSemisimple_torsionBy_of_irreducible, SimpleGraph.card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix, Ideal.map_spanIntNorm, eq_isotypicComponent_iff, groupHomology.mem_cycles₁_of_comp_eq_d₂₁, RootPairing.coroot'In_rootSpanMem_eq_pairingIn, Ideal.IsPrime.pow_mem_iff_mem, exteriorPower.alternatingMapLinearEquiv_ιMulti, KaehlerDifferential.kerToTensor_apply, Subspace.forall_mem_dualAnnihilator_apply_eq_zero_iff, coe_subtypeL', DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, Finsupp.mem_span_iff_linearCombination, coe_sup, Polynomial.degreeLT.basis_val, selfAdjointPart_comp_subtype_skewAdjoint, setBasisOfLinearIndependentOfCardEqFinrank_repr_apply, IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule, Algebra.Presentation.differentials.hom₁_single, LinearMap.rank_eq_of_surjective, RingOfIntegers.exponent_eq_sInf, RingHom.SurjectiveOnStalks.exists_mul_eq_tmul, TensorProduct.quotientTensorQuotientEquiv_symm_apply_mk_tmul, Algebra.zariskisMainProperty_iff, Algebra.Generators.exists_presentation_of_basis_cotangent, lift_rank_range_of_injective, Ideal.mem_toCotangent_ker, groupCohomology.mem_cocycles₁_of_addMonoidHom, groupCohomology.cocycles₂.d₂₃_apply, ProperCone.mem_map, one_mem_div, isArtinian_iff_submodule_quotient, PeriodPair.hasSum_derivWeierstrassPExcept, IsLocalization.coe_primeSpectrumOrderIso_symm_apply_asIdeal, Ideal.Filtration.mem_submodule, LinearMap.IsSymmetric.directSum_decompose_apply, mem_torsion_iff, linearProjOfIsCompl_comp_surjective_of_exact, dualCopairing_eq, EuclideanGeometry.reflection_vadd_smul_vsub_orthogonalProjection, Nat.exists_mem_span_nat_finset_of_ge, LieSubmodule.mem_mk_iff', ringKrullDim_quotient, Ideal.finsuppTotal_apply_eq_of_fintype, groupHomology.isoCycles₁_inv_comp_iCycles_apply, reflection_singleton_apply, rank_span_set, PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, RootPairing.RootPositiveForm.zero_lt_posForm_iff, IsCompl.projection_apply_left, eq_isotypicComponent_of_le, groupCohomology.map_H0Iso_hom_f_apply, LieModule.Cohomology.twoCochain_alt, EuclideanGeometry.inter_eq_singleton_orthogonalProjection, PointedCone.coe_map, groupCohomology.H0IsoOfIsTrivial_inv_apply, ContinuousLinearMap.mkOfIsCompactOperator_mem_compactOperator, LinearMap.mem_skewAdjointSubmodule, quotDualCoannihilatorToDual_nondegenerate, rank_bot, Ideal.mem_iff_of_associated, LieSubmodule.mem_toSubmodule, mem_dualAnnihilator, mem_ideal_smul_span_iff_exists_sum', coeff_minpolyDiv_sub_pow_mem_span, groupHomology.chains₁ToCoinvariantsKer_surjective, ZLattice.comap_discreteTopology, adjoin_monomial_eq_reesAlgebra, InnerProductSpace.gramSchmidt_def, LinearMap.submoduleMap_coe_apply, ContinuousLinearMap.isComplete_ker, Module.End.mem_invtSubmodule_iff_mapsTo, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem, biUnion_associatedPrimes_eq_compl_regular, ContinuousMap.mem_idealOfSet, Algebra.Extension.lTensor_cotangentComplex_eq_cotangentComplexBaseChange, AffineSubspace.linear_topEquiv, prod_coe, DirectSum.decompose_eq_mul_idempotent, toLinearPMap_range, Affine.Simplex.orthogonalProjectionSpan_eq_point, coe_dualCoannihilator_span, LieHom.quotKerEquivRange_toFun, isSimpleModule_iff_isAtom, FiniteDimensional.span_of_finite, MeasureTheory.MemLp.condExpL2_ae_eq_condExp, HahnEmbedding.Partial.archimedeanClassMk_eq_iff, mem_vectorSpan_iff_eq_weightedVSub, TensorProduct.map₂_eq_range_lift_comp_mapIncl, Module.End.mapsTo_genEigenspace_of_comm, isArtinian_of_le, exteriorPower.ιMulti_span_of_span, biSup_comap_subtype_eq_top, MonoidAlgebra.of_mem_span_of_iff, IsLocalRing.residue_eq_zero_iff, PointedCone.subset_dual_dual, Polynomial.mem_iff_eq_smul_annIdealGenerator, IsLinearTopology.hasBasis_open_submodule, FractionalIdeal.isNoetherian_coeIdeal, RootPairing.injOn_dualMap_subtype_span_root_coroot, MvPolynomial.mem_pow_idealOfVars_iff, LinearMap.range_domRestrict_eq_range_iff, LinearMap.sub_mem_ker_iff, Ideal.finsuppTotal_apply, TensorProduct.exists_finite_submodule_of_finite', biSup_eq_range_dfinsupp_lsum, IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe, Rep.resCoindAdjunction_unit_app_hom_hom, groupCohomology.mem_cocycles₁_def, IsOrtho.orthogonalProjection_comp_subtypeL, RootPairing.restrictScalars_pairing, EuclideanGeometry.orthogonalProjection_map, Ideal.subset_union_prime', Algebra.adjoin_span, LieModule.Cohomology.d₂₃_apply, LieAlgebra.InvariantForm.restrict_nondegenerate, exteriorPower.alternatingMapLinearEquiv_symm_map, span_range_inclusion_restrictScalars_eq_top, isNoetherian_submodule, selfAdjointPart_comp_subtype_selfAdjoint, AffineSubspace.vsub_mem_direction, HasStrictFDerivAt.eq_implicitFunctionOfComplemented, exteriorPower.instFree, Affine.Simplex.circumradius_restrict, DividedPowers.mem_dpEqualizer_iff, PrimeSpectrum.union_zeroLocus, mulMap_comm, HahnEmbedding.Seed.baseEmbedding_strictMono, AlgebraicGeometry.Scheme.zeroLocus_biInf, Module.Flat.out, RootPairing.finrank_rootSpan_map_polarization_eq_finrank_corootSpan, LieModule.Cohomology.d₁₂_apply_apply, Affine.Simplex.medial_restrict, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, FiniteDimensional.mem_span_of_iInf_ker_le_ker, equivSubtypeMap_symm_apply, mem_prod, botEquivPUnit_apply, LinearMap.ofIsComplProd_apply, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, AffineIndependent.finrank_vectorSpan_add_one, coe_orthogonalDecomposition_symm, groupCohomology.mapCocycles₂_comp_i_apply, Projectivization.finrank_submodule, ker_subtype, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_apply, MeasureTheory.aestronglyMeasurable_condExpL2, Ideal.absNorm_mem, orthogonalProjection_bot, BoxIntegral.unitPartition.integralSum_eq_tsum_div, groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂, ZLattice.module_finite, EuclideanGeometry.angle_orthogonalProjection_self, mem_pi, EuclideanGeometry.orthogonalProjection_apply_mem, isNoetherian_of_le, IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite, coe_isComplEquivProj_symm_apply, finrank_add_inf_finrank_orthogonal, groupHomology.cycles₁IsoOfIsTrivial_hom_apply, exists_add_mem_mem_orthogonal, LieAlgebra.bracket_ofTwoCocycle, LinearMap.exact_subtype_mkQ, coe_torsion', AffineSubspace.coe_subtypeₐᵢ, Algebra.Extension.Cotangent.val_mk, isClosed_topologicalClosure, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_succ_sub_seq_mem, PeriodPair.latticeBasis_zero, linearDisjoint_iff, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn, GradedTensorProduct.auxEquiv_one, mem_bot, tendsto_card_div_pow_atTop_volume, toLocalized₀_apply_coe, MvPolynomial.weightedDecomposition.decompose'_apply, EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq, LinearMap.IsSymm.domRestrict, Module.End.mem_eigenspace_intrinsicStar_iff, Subspace.finrank_dualCoannihilator_eq, apply_mem_span_image_iff_mem_span, sup_eq_range, mem_map, mem_div_iff_forall_mul_mem, MeasureTheory.condExpL2_indicator_ae_eq_smul, exteriorPower.ιMultiDual_apply_diag, Representation.instIsTrivialSubtypeMemSubgroupSubmoduleInvariantsCompLinearMapIdSubtypeToInvariants, RootPairing.finrank_corootSpanIn_int, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, Algebra.TensorProduct.linearEquivIncludeRange_toLinearMap, SModEq.zero, IsLocalRing.mem_maximalIdeal, retractionOfSectionOfKerSqZero_comp_kerToTensor, PadicInt.exists_mem_range, groupCohomology.cocycles₂_map_one_fst, MvPolynomial.monomial_mul_mem_coeffsIn, groupCohomology.mapCocycles₂_comp_i_assoc, rank_quotient_add_rank, Ideal.toCotangent_range, FractionalIdeal.mem_coeSubmodule, PrimeSpectrum.zeroLocus_subset_zeroLocus_iff, Module.Invertible.exists_linearEquiv_ideal, ZLattice.rank, Subspace.finiteDimensional_quot_dualCoannihilator_iff, groupCohomology.H1IsoOfIsTrivial_inv_apply, HasStrictFDerivAt.mem_implicitToPartialHomeomorphOfComplemented_target, PeriodPair.ω₂_div_two_notMem_lattice, IsLocalization.AtPrime.coe_primeSpectrumOrderIso_apply_coe_asIdeal, LieSubalgebra.mem_toSubmodule, coe_toConvexCone, Module.Baer.ExtensionOf.is_extension, Localization.exists_finite_awayMapₐ_of_surjective_awayMapₐ, FirstOrder.Field.lift_genericMonicPoly, mem_finset_inf, GradedTensorProduct.tmul_coe_mul_one_tmul, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField, SubmodulesBasis.smul, PeriodPair.hasSum_derivWeierstrassP, groupHomology.mapCycles₁_id_comp_assoc, Subalgebra.mem_toSubmodule, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, rank_submodule_le_one_iff, PeriodPair.compl_lattice_diff_singleton_mem_nhds, AffineIndependent.card_le_finrank_succ, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, Coplanar.finrank_le_two, LocalizedModule.mem_ker_mkLinearMap_iff, Algebra.Generators.exists_presentation_of_free_cotangent, goursat, Ideal.iSup_eq_span, coe_prodEquivOfIsCompl', Affine.Simplex.finrank_direction_altitude, PeriodPair.hasSumLocallyUniformly_derivWeierstrassP, groupCohomology.mem_cocycles₁_of_comp_eq_d₀₁, HahnEmbedding.Seed.strictMono_coeff, subtypeₗᵢ_toLinearMap, groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, mem_span_finset, Module.Basis.sumQuot_repr_left, mem_skewAdjointMatricesSubmodule', LinearEquiv.ofSubmodules_apply, LinearMap.lTensor_range, groupCohomology.H2π_comp_map_apply, groupHomology.mapCycles₁_comp, topEquiv_apply, Module.isTorsionBySet_annihilator, PrimeSpectrum.zeroLocus_span, Polynomial.degreeLT.addLinearEquiv_castAdd, subtype_apply, GradedTensorProduct.tmul_coe_mul_coe_tmul, Ideal.powQuotSuccInclusion_apply_coe, LinearEquiv.toSpanNonzeroSingleton_homothety, RootPairing.Base.exists_mem_span_pairingIn_ne_zero_and_pairwise_ne, MeasureTheory.integral_condExpL2_eq, Representation.Coinvariants.sub_mem_ker, finiteDimensional_vectorSpan_image_of_finite, RootPairing.instFiniteSubtypeMemSubmoduleRootSpanOfFinite, LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful, orzechProperty_iff, Affine.Simplex.ninePointCircle_restrict, Algebra.Extension.H1Cotangent.val_zero, Nat.subset_span_setGcd, exists_forall_notMem_of_forall_ne_top, IsAdic.hasBasis_nhds, submodule_eq_sSup_le_nonzero_spans, LinearMap.tensorKerEquivOfSurjective_symm_tmul, RootPairing.Base.coroot_mem_span_int, groupCohomology.toCocycles_comp_isoCocycles₂_hom, LinearMap.IsProj.eq_conj_prodMap, LinearMap.tensorEqLocus_coe, LinearDisjoint.not_linearIndependent_pair_of_flat_right, mem_comap, length_lt, PrimeSpectrum.isClosed_iff_zeroLocus_radical_ideal, finrank_lt_finrank_of_lt, LinearIsometry.isComplete_map_iff, LinearMap.mem_submoduleImage_of_le, Polynomial.degreeLT.addLinearEquiv_apply_fst, mulLeftMap_apply, ZLattice.covolume.tendsto_card_div_pow, MeasureTheory.setIntegral_condExpL2_indicator, IsLocalization.isMaximal_iff_isMaximal_disjoint, PeriodPair.mem_lattice, ModuleCat.imageIsoRange_hom_subtype, IsLinearTopology.hasBasis_submodule, stereographic_apply_neg, instCountable_of_discrete_submodule, OrthonormalBasis.orthogonalProjection_apply_eq_sum, groupHomology.mapCycles₁_comp_i, LinearMap.toKerLocalized_isLocalizedModule, submoduleOf_sup_of_le, Affine.Simplex.face_restrict, rank_range_le, LieSubalgebra.engel_carrier, ClosedSubmodule.mem_toSubmodule_iff, DirectSum.coeLinearMap_of, ContinuousLinearMap.coe_equivRange, rank_le, coe_prodEquivOfIsCompl, groupCohomology.shortComplexH0_f, DirectSum.coeLinearMap_eq_dfinsuppSum, HahnEmbedding.Partial.orderTop_eq_iff, RootPairing.polarizationIn_Injective, finrank_vectorSpan_insert_le, LinearIsometryEquiv.coe_ofEq_apply, PeriodPair.analyticOnNhd_derivWeierstrassPExcept, groupCohomology.cocyclesOfIsCocycle₁_coe, Subspace.dualPairing_nondegenerate, Affine.Simplex.interior_restrict, Ideal.map_relNorm, vsub_rev_mem_vectorSpan_pair, Polynomial.mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero, ExteriorAlgebra.GradedAlgebra.ι_sq_zero, ProjectiveSpectrum.subset_zeroLocus_iff_le_vanishingIdeal, mul_mem_smul_iff, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem, Ideal.span_singleton_mul_eq_span_singleton_mul, RootPairing.finrank_rootSpanIn_int, AddMonoidAlgebra.decomposeAux_coe, LinearMap.ker_rangeRestrict, CliffordAlgebra.evenOdd.gradedMonoid, smul_subset_smul, LinearMap.IsSymmetric.card_filter_eigenvalues_eq, FiniteDimensional.RCLike.properSpace_submodule, Ideal.isTorsionBySet_cotangent, range_stereographic_symm, AffineSubspace.inclusion_linear, ProjectiveSpectrum.union_zeroLocus, AddMonoidAlgebra.gradeBy.isInternal, MvPolynomial.mul_X_mem_coeffsIn, Module.Flat.iff_rTensor_injective, HasStrictFDerivAt.to_implicitFunctionOfComplemented, EuclideanGeometry.orthogonalProjection_apply', CliffordAlgebra.involute_mem_evenOdd_iff, Affine.Simplex.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, Rep.subtype_hom, isOpenEmbedding_stereographic_symm, TensorProduct.Algebra.exists_of_fg, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le, Set.Finite.submoduleSpan, Rep.coindVEquiv_symm_apply_coe, IsNoetherianRing.isClosed_ideal, EuclideanGeometry.Sphere.coe_secondInter, Ideal.map_includeRight_eq, finiteDimensional_sup, isIsotypic_submodule_iff, finiteDimensional_direction_map, PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, torsionBy_torsionBy_eq_top, coe_span_smul, TensorProduct.exists_finite_submodule_left_of_setFinite, TensorProduct.quotientTensorEquiv_symm_apply_mk_tmul, groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply, LinearEquiv.mem_dilatransvections_iff_rank, ModuleCat.imageIsoRange_inv_image_ι_apply, basisOfLinearIndependentOfCardEqFinrank_repr_apply, mem_pairSelfAdjointMatricesSubmodule', ContinuousLinearMap.isClosed_ker, MvPolynomial.X_mul_mem_coeffsIn, EuclideanGeometry.orthogonalProjection_orthogonalProjection_of_le, Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial, IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one, strictMono_comap_prod_map, Matrix.cRank_toNat_eq_finrank, ContinuousMap.idealOfSet_closed, mem_annihilator', HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_target, groupCohomology.coboundaries₂.val_eq_coe, RootPairing.PolarizationIn_eq, EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection, adjoint_subtypeL, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, instIsTwoSidedColonCoe, ext_iff, Ideal.disjoint_powers_iff_notMem, Module.Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul, dualRestrict_ker_eq_dualAnnihilator, LinearIsometry.equivRange_apply_coe, mem_left_iff_eq_zero_of_disjoint, FiniteDimensional.span_finset, reflection_orthogonalComplement_singleton_eq_neg, lipschitzGroup.conjAct_smul_ι_mem_range_ι, Subalgebra.finrank_toSubmodule, groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂, sub_mem_pNilradical_iff_pow_expChar_pow_eq, MvPolynomial.IsHomogeneous.HomogeneousSubmodule.gcommSemiring, Affine.Triangle.dist_circumcenter_reflection_orthocenter, MeasureTheory.norm_condExpL2_coe_le, isArtinian_span_of_finite, MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, IsIsotypic.isotypicComponent, LinearMap.finrank_range_of_inj, MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable, LinearMap.toPMap_apply, groupCohomology.d₁₂_apply_mem_cocycles₂, Rep.invariantsAdjunction_unit_app, groupHomology.mapCycles₂_id_comp, coe_linearProjOfIsCompl_apply, inclusion_apply, UniqueDiffWithinAt.dense_tangentConeAt, LinearMap.linearProjOfIsCompl_apply_right, ArchimedeanClass.mem_ball_iff, groupCohomology.d₀₁_apply_mem_cocycles₁, mem_smul_iff_inv_mul_mem, LinearEquiv.ofLeftInverse_symm_apply, LinearMap.range_rangeRestrict, isNoetherian_iff_submodule_quotient, ZSpan.repr_ceil_apply, PowerSeries.coe_hasEvalIdeal, RingHom.mem_ker, ZLattice.comap_equiv_apply, surjective_tensorToSpan, PrimeSpectrum.mem_compl_zeroLocus_iff_notMem, PrimeSpectrum.zeroLocus_radical, mem_torsionBySet_iff, PrimeSpectrum.zeroLocus_minimalPrimes, Ideal.mem_span_range_self, torsion_torsion_eq_top, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff', LinearIsometryEquiv.ofTop_toLinearEquiv, finrank_span_le_card, coe_ofClass, isLocalizedModule, range_subtypeL, PrimeSpectrum.isIrreducible_zeroLocus_iff, botEquivPUnit_symm_apply, Module.Basis.addSubgroupOfClosure_repr_apply, isSMulRegular_submodule_iff_right_eq_zero_of_smul, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, groupCohomology.subtype_comp_d₀₁_apply, PeriodPair.isClosed_lattice, linearIndependent_fin_cons, Module.length_top, IsDedekindDomain.exists_forall_sub_mem_ideal, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, IsDedekindDomain.HeightOneSpectrum.valuation_def, contDiffOn_stereoToFun, spinGroup.conjAct_smul_ι_mem_range_ι, image_span_subset_span, ValuativeRel.supp_def, MonoidAlgebra.mem_span_support, GradedTensorProduct.auxEquiv_symm_one, groupCohomology.H2π_eq_iff, NumberField.det_basisOfFractionalIdeal_eq_absNorm, GradedTensorProduct.auxEquiv_comm, LinearMap.comap_leq_ker_subToSupQuotient, HilbertBasis.hasSum_orthogonalProjection, smul_coe_torsionBy, LinearMap.rTensor_injective_iff_subtype, MeasureTheory.mem_lpMeas_indicatorConstLp, stereoInvFun_apply, Ideal.image_subset_nonunits_valuationSubring, HahnEmbedding.IsPartial.strictMono, collinear_iff_finrank_le_one, mem_annihilator, groupCohomology.cocycles₂_map_one_snd, mem_set_smul_def, Ideal.disjoint_map_primeCompl_iff_comap_le, LinearIsometryEquiv.ofTop_symm_apply_coe, LinearMap.submoduleImage_apply_of_le, LinearRecurrence.solSpace_rank, LieSubalgebra.coe_toSubmodule, LinearEquiv.ofSubmodule'_symm_apply, groupHomology.toCycles_comp_isoCycles₁_hom_apply, AffineIsometryEquiv.coe_ofEq_apply, IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp, closed_of_finiteDimensional, Representation.mem_invariants_iff_of_forall_mem_zpowers, spinGroup.involute_act_ι_mem_range_ι, Ideal.IsMaximal.isClosed, Affine.Simplex.altitude_restrict_eq_comap_subtype, MeasureTheory.lintegral_nnnorm_condExpL2_le, PeriodPair.periodic_derivWeierstrassP, exteriorPower.finrank_eq, ContinuousLinearMap.eqOn_closure_span, AffineSubspace.isometryEquivMap.toAffineMap_eq, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff, groupHomology.mapCycles₂_comp_i, AffineSubspace.signedInfDist_eq_signedDist_of_mem, Polynomial.degreeLT.addLinearEquiv_apply_snd, IsLocalization.mk'_mem_iff, ClassGroup.mkMMem_surjective, Finsupp.mem_submodule_iff, groupCohomology.map_H0Iso_hom_f, mem_span_singleton, LinearMap.finrank_genEigenspace_le, codisjoint_iff_exists_add_eq, Module.Basis.sumQuot_repr_inl, LinearMap.IsSymmetric.diagonalization_symm_apply, CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_zero_iff, AddMonoidAlgebra.mem_ideal_span_of'_image, groupHomology.boundariesOfIsBoundary₁_coe, LieModule.weight_vector_multiplication, Affine.Simplex.signedInfDist_apply_self, iInf_coe, Representation.mem_invariants, LinearMap.quotientInfEquivSupQuotient_apply_mk, WittVector.mem_span_p_pow_iff_le_coeff_eq_zero, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, SimpleGraph.linearIndependent_lapMatrix_ker_basis_aux, finiteDimensional_vectorSpan_of_finite, Nat.finite_setOf_setGcd_dvd_and_mem_span, finiteQuotient_iff, Ideal.IsPrime.one_notMem, groupCohomology.π_comp_H1Iso_hom, LieAlgebra.mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg, RootPairing.corootSpanMem_reflectionPerm_self, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, Ideal.mem_of_liesOver, Module.isTorsionBySet_span_singleton_iff, smoothSheafCommRing.isUnit_stalk_iff, Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes, LinearIsometryEquiv.reflections_generate, AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection, Subrepresentation.mem_asSubmodule'_iff, exteriorPower.map_apply_ιMulti_family, NumberField.mixedEmbedding.span_idealLatticeBasis, HomogeneousSubmodule.mem_toSubmodule_iff, RingPreordering.mem_support, ExteriorAlgebra.ιMulti_range, AffineEquiv.linear_ofEq, norm_orthogonalProjection_apply_le, instPolynormableSpaceSubtypeMemSubmodule, HasStrictFDerivAt.map_implicitFunction_eq, AffineSubspace.coe_direction_eq_vsub_set, Algebra.Extension.Hom.sub_one_tmul, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc_apply, IsLinearTopology.hasBasis_open_ideal, GradedAlgebra.proj_recompose, mem_span_iff_exists_finset_subset, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff, apply_coe_mem_map, OrthonormalBasis.starProjection_eq_sum_rankOne, Ideal.isTwoSided_iff, LinearMap.BilinForm.apply_apply_same_eq_zero_iff, PointedCone.mem_dual, mem_iSup_iff_exists_dfinsupp, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff, FDRep.average_char_eq_finrank_invariants, Algebra.zariskisMainProperty_iff', groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv, AffineIsometryEquiv.ofTop_symm_apply_coe, LinearIndepOn.subset_span_extend, isArtinian_range, TopologicalSpace.IsSeparable.span, ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier, TensorProduct.inner_mapIncl_mapIncl, RootPairing.toLinearMap_apply_PolarizationIn, IsDiscreteValuationRing.isOpen_iff, exteriorPower.zeroEquiv_naturality, instNonUnitalSubsemiringClassIdeal, Collinear.finiteDimensional_direction_affineSpan, KaehlerDifferential.D_apply, finiteDimensional_direction_affineSpan_insert_set, TensorProduct.exists_finite_submodule_right_of_setFinite, HahnEmbedding.IsPartial.truncLT_mem_range, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply_ker, groupHomology.single_one_fst_sub_single_one_fst_mem_boundaries₂, Affine.Simplex.orthogonalProjectionSpan_congr, LinearIndependent.linearCombinationEquiv_apply_coe, Polynomial.adjSylvester_comp_sylveserMap, IsLocalization.algebraMap_mem_map_algebraMap_iff, mapsTo_smul_closure, iSup_eq_range_dfinsupp_lsum, Module.Basis.span_apply, Ideal.eq_span_singleton_mul, LieModule.Cohomology.twoCochain_skew, AffineSubspace.mem_direction_iff_eq_vsub, mem_conductor_iff, HasStrictFDerivAt.implicitToPartialHomeomorph_self, MeasureTheory.lpMeasToLpTrimLie_symm_indicator, ContinuousLinearMap.closed_complemented_range_of_isCompl_of_ker_eq_bot, groupHomology.mapCycles₁_id_comp_apply, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_assoc, Associates.le_singleton_iff, CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, RootPairing.instFiniteSubtypeMemSubmoduleCorootSpanOfFinite, AffineIsometryEquiv.ofEq_symm, ContinuousLinearMap.equivRange_symm_apply, RootPairing.finrank_corootSpanIn, LinearIndependent.linearCombination_comp_repr, Ideal.mem_map_of_equiv, coe_restrictScalars, Representation.coe_coindV, coe_inclusion, LinearIsometry.extend_apply, NumberField.FinitePlace.norm_lt_one_iff_mem, Module.support_of_algebra, instLocallyConvexSpaceSubtypeMemSubmodule, Polynomial.degreeLT.instFiniteSubtypeMemSubmodule, KaehlerDifferential.one_smul_sub_smul_one_mem_ideal, IsSMulRegular.notMem_of_mem_minimalPrimes, finrank_strictMono, Module.End.IsSemisimple.restrict, exists_linearIndepOn_extension, comap_coe, Algebra.Extension.Cotangent.mk_eq_zero_iff, Rat.valuation_le_one_iff_den, LinearMap.BilinForm.mem_dualSubmodule, asymptoticCone_affineSubspace, linearEquiv_det_reflection, groupCohomology.instEpiModuleCatH1π, PeriodPair.differentiableOn_derivWeierstrassP, LinearPMap.apply_comp_inclusion, PeriodPair.weierstrassPExcept_def, GradedTensorProduct.tmul_one_mul_coe_tmul, Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton, mk_mem_projectivization_iff, coe_pointwise_smul, Coplanar.finiteDimensional_direction_affineSpan, IsSemisimpleModule.sup, Matrix.rank_eq_finrank_range_toLin, Affine.Simplex.ExcenterExists.touchpointWeights_restrict, PrimeSpectrum.mem_zeroLocus, groupCohomology.H2π_comp_map, Matrix.eRank_toNat_eq_finrank, LinearPMap.sSup_apply, CharacterModule.intSpanEquivQuotAddOrderOf_apply, Ideal.mapCotangent_toCotangent, groupHomology.π_comp_H2Iso_hom, AffineSubspace.instIsTopologicalAddTorsorSubtypeMemSubmoduleDirection, stereoToFun_apply, uniqueDiffWithinAt_iff, IsPrincipal.mem_iff_eq_smul_generator, sub_starProjection_mem_orthogonal, LinearPMap.snd_apply, prodEquivOfIsCompl_symm_apply_fst_eq_zero, IsLocalization.isPrime_iff_isPrime_disjoint, PrimeSpectrum.zeroLocus_subset_zeroLocus_singleton_iff, NumberField.mixedEmbedding.mem_span_latticeBasis, exteriorPower.ιMulti_apply_coe, affineIndependent_iff_not_finrank_vectorSpan_le, coe_tensorSpanEquivSpan_apply_tmul, annihilator_map_mkQ_eq_colon, LieSubmodule.mem_baseChange_iff, SModEq.sub_mem, FG.lTensor.directLimit_apply', PowerBasis.mem_span_pow', PrimeSpectrum.subset_vanishingIdeal_zeroLocus, dualRestrict_def, ContinuousLinearMap.coe_projKerOfRightInverse_apply, Rep.coindToInd_apply, groupHomology.mapCycles₁_comp_i_apply, IsLocalization.AtPrime.to_map_mem_maximal_iff, Module.Basis.SmithNormalForm.snf, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupHomology.mapCycles₂_comp, mem_span_C_coeff, AlgHom.toKerIsLocalization_apply, SetLike.homogeneous_zero_submodule, ModuleCat.kernelIsoKer_inv_kernel_ι_apply, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop, Ideal.mem_sInf, Nat.mem_maximalIdeal_iff, IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite, MvPolynomial.DirectSum.coeAddMonoidHom_eq_support_sum, HahnEmbedding.Partial.truncLT_mem_range_sSupFun, Ideal.IsPrime.prod_mem_iff, Ideal.mem_quotient_iff_mem, FG.rTensor.directLimit_apply, PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal, AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty, groupCohomology.isoCocycles₂_hom_comp_i, coe_continuous_linearProjOfClosedCompl, EuclideanGeometry.orthogonalProjection_subtype, LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_source, LieModule.Cohomology.d₁₂_apply_coe_apply_apply, coe_orthogonalDecomposition, EuclideanGeometry.two_zsmul_oangle_self_orthogonalProjection, rank_submodule_le_one_iff', mem_singleton_set_smul, groupCohomology.π_comp_H0Iso_hom_apply, IsSMulRegular.submodule, finiteDimensional_direction_affineSpan_insert, StrongDual.polarSubmodule_eq_polar, finrank_orthogonal_span_singleton, inclusionSpan_apply_coe, groupHomology.coe_mapCycles₂, coe_topologicalNilradical, small_span_singleton, comap_subtype_self, exteriorPower.oneEquiv_naturality, NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top, SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux, one_le_finrank_iff, IsLocalizedModule.mem_ker_iff, groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply, groupHomology.H1π_comp_map_apply, MvPolynomial.mem_pow_idealOfVars_iff', Affine.Simplex.ExcenterExists.excenter_restrict, LinearMap.mem_eqLocus, norm_subtypeL, RootPairing.posRootForm_posForm_pos_of_ne_zero, mem_orthogonal', biUnion_associatedPrimes_eq_zero_divisors, LinearPMap.sub_apply, Module.Flat.eqLocus_lTensor_eq, LinearMap.lift_rank_eq_of_surjective, Subspace.dualRestrict_leftInverse, TensorProduct.exists_finite_submodule_left_of_finite, Ideal.mem_jacobson_iff, IsCompl.projection_eq_self_iff, Module.instFiniteSubtypeMemIdealOfIsNoetherian, AffineSubspace.toContinuousAffineMap_subtypeₐᵢ, rank_mono, LieModule.Cohomology.mem_twoCochain_iff, ContinuousLinearMap.coe_rangeRestrict, setLike.coe_galgebra_toFun, norm_sq_eq_add_norm_sq_projection, finiteDimensional_direction_affineSpan_range, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem_mul, Polynomial.det_taylorLinearEquiv_toLinearMap, traceDual_le_span_map_traceDual, linearDepOn_iff, ContinuousLinearMap.equivRange_symm_toLinearEquiv, MvPolynomial.decompose'_apply, Ideal.mul_le, mem_colon_iff_le, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom, TwoSidedIdeal.mem_fromIdeal, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, LinearEquiv.ofInjective_apply, Module.length_submodule, FiniteArchimedeanClass.mem_ball_iff, comm_trans_rTensorOne, starProjection_apply, card_quotient_mul_card_quotient, AlgebraicGeometry.Scheme.zeroLocus_radical, FractionalIdeal.isNoetherian_spanSingleton_inv_to_map_mul, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_target, coe_finsetInf, StandardEtalePair.existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_bot, linearIndependent_span, WittVector.mem_ker_truncate, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_self, mem_span_set, MatrixModCat.toModuleCat_obj_carrier, Subspace.flip_quotDualCoannihilatorToDual_bijective, PrimeSpectrum.zeroLocus_ideal_mem_irreducibleComponents, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, comap_equiv_self_of_inj_of_le_apply, rank_quotient_add_rank_of_isDomain, pinGroup.conjAct_smul_ι_mem_range_ι, groupCohomology.cocycles₁_map_inv, exists_fg_le_subset_range_rTensor_subtype, DirectSum.coeAlgHom_of, TensorProduct.rTensor_injective_of_forall_vanishesTrivially, isArtinian_of_fg_of_artinian, set_smul_eq_map, Polynomial.annIdealGenerator_mem, Affine.Triangle.dist_orthocenter_reflection_circumcenter, groupCohomology.mapCocycles₁_one, Ideal.symm_apply_mem_of_equiv_iff, IsDedekindDomain.HeightOneSpectrum.intAdicAbv_lt_one_iff, RingHom.toKerIsLocalization_apply, LinearMap.coe_range, EuclideanGeometry.oangle_orthogonalProjection_self, Affine.Simplex.map_altitude_restrict, LinearMap.mem_span_iff_continuous_of_finite, MvPolynomial.monomial_mem_pow_idealOfVars_iff, Ideal.mem_leadingCoeff, Affine.Simplex.faceOpposite_restrict, groupHomology.H2π_comp_map_assoc, neg_mem_iff, Polynomial.degreeLT.addLinearEquiv_apply, PrimeSpectrum.zeroLocus_iSup, Ideal.ResidueField.exists_smul_eq_tmul_one, fst_orthogonalDecomposition_apply, LinearEquiv.mem_dilatransvections_iff_finrank, DividedPowers.RatAlgebra.dpow_apply, Matrix.rank_eq_finrank_span_row, RootPairing.prod_rootForm_smul_coroot_mem_range_domRestrict, smul_starProjection_singleton, Polynomial.mem_annIdeal_iff_aeval_eq_zero, PeriodPair.hasSumLocallyUniformly_weierstrassPExcept, finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply, PointedCone.convex, LinearEquiv.ofSubmodules_symm_apply, IsSemisimpleModule.exists_quotient_linearEquiv_submodule, Ideal.homogeneousHull_eq_iSup, Matrix.isRepresentation.toEnd_exists_mem_ideal, LinearMap.kerComplementEquivRange_apply_coe, mem_mul_span_singleton, mem_span_finset', restrictScalarsEquiv_symm_apply, mem_span_singleton_self, finiteDimensional_vectorSpan_insert_set, LinearMap.quotientInfEquivSupQuotient_injective, map₂_eq_span_image2, IsAdic.hasBasis_nhds_zero, isArtinian_of_submodule_of_artinian, Module.Basis.restrictScalars_repr_apply, CliffordAlgebra.GradedAlgebra.ι_apply, orthogonalFamily_self, EuclideanGeometry.dist_orthogonalProjection_eq_dist_iff_eq_of_mem, LieModule.Cohomology.d₁₂_apply_apply_ofTrivial, GradedTensorProduct.auxEquiv_mul, IsSelfAdjoint.dense_domain, AlgebraicGeometry.Scheme.zeroLocus_inf, lTensorOne'_tmul, image_comap_zeroLocus_eq_zeroLocus_comap, RootPairing.CoPolarizationIn_eq, affineSpan_subset_span, AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert, Affine.Simplex.exradius_restrict, Subrepresentation.mem_asSubmodule_iff, rTensorOne'_tmul_one, inner_orthogonalProjection_eq_of_mem_right, DirectSum.decompose_symm_algebraMap, LinearMap.ker_domRestrict, ContinuousMap.adjoin_id_eq_span_one_union, ContinuousMap.AlgHom.closure_ker_inter, Subbimodule.coe_mk, finiteDimensional_vectorSpan_singleton, reesAlgebra.monomial_mem, PrimeSpectrum.zeroLocus_eq_iff, exists_max_ideal_of_mem_nonunits, rTensorOne'_tmul, isScalarTower', finiteDimensional_inf_right, Finsupp.linearCombinationOn_range, Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex, colon_span, LinearPMap.coe_smul, coe_mem, TensorProduct.exists_finite_submodule_right_of_setFinite', Ideal.isCompact_of_fg, realPart_comp_subtype_selfAdjoint, groupCohomology.π_comp_H0Iso_hom_assoc, ZSpan.coe_floor_self, projective_units, RootPairing.algebraMap_rootFormIn, Ideal.mem_matrix, TwoSidedIdeal.mem_asIdealOpposite, RingPreordering.one_notMem_support, map_subtype_embedding_eq, MvPolynomial.mem_restrictDegree, ModuleCat.imageIsoRange_hom_subtype_assoc, groupCohomology.mem_cocycles₂_iff, FractionalIdeal.mem_coeIdeal, LinearDisjoint.injective, baseChange_eq_span, ZLattice.module_free, LinearMap.mem_submoduleImage, dualCopairing_apply, LinearEquiv.toSpanNonzeroSingleton_apply, IsLocalization.mk'_mem_map_algebraMap_iff, Affine.Simplex.orthogonalProjection_circumcenter, mem_span_insert', finite_iff_ideal_quotient, Ideal.coe_restrictScalars, Module.Flat.instSubalgebraToSubmodule, ContinuousLinearMap.coe_linearMap_equivRange, Ideal.mk_mem_cotangentIdeal, LinearPMap.map_zero, MvPolynomial.indicator_mem_restrictDegree, coe_mapAlgEquiv_apply, LinearMap.BilinForm.nondegenerate_restrict_iff_disjoint_ker, LinearPMap.map_add, LinearIndependent.notMem_span, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', LinearIsometryEquiv.completeSpace_map, groupCohomology.H2π_comp_map_assoc, HahnEmbedding.ArchimedeanStrata.nontrivial_stratum, conductor_subset_adjoin, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, ker_inclusion, AffineIndependent.finrank_vectorSpan_image_finset, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_liftK_hom, FractionalIdeal.isNoetherian_zero, groupHomology.mapCycles₂_comp_apply, DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top, Algebra.adjoin_toSubmodule_le, LinearIsometryEquiv.toSpanUnitSingleton_apply, comap_subtype_eq_top, AffineSubspace.subtypeA_toAffineMap, Ideal.isOpen_pow_of_isMaximal, LinearIndependent.span_repr_eq, Affine.Simplex.exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter, norm_inner_eq_norm_tfae, RootPairing.rootForm_self_eq_zero_iff, prodEquivOfIsCompl_symm_apply, Rep.coindFunctorIso_inv_app_hom_hom_apply_coe, Module.End.hasEigenvector_iff, injective_tensorToSpan, Ideal.mem_leadingCoeffNth, projective_of_isUnit, PeriodPair.derivWeierstrassP_sub_coe, Module.Basis.restrictScalars_apply, RootPairing.invtRootSubmodule.eq_bot_iff, instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent, HasStrictFDerivAt.to_implicitFunction, exteriorPower.ιMultiDual_apply_ιMulti, natAbs_det_equiv, Algebra.zariskisMainProperty_iff_exists_saturation_eq_top, Module.Basis.mem_submodule_iff', Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver, MvPolynomial.pointToPoint_zeroLocus_le, Module.End.IsFinitelySemisimple.restrict, map_subtype_span_singleton, Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq, Ideal.isMaximal_iff, LinearPMap.adjointDomainMkCLM_apply, LinearPMap.mem_domain_iff, PointedCone.mem_map, LocalizedModule.exists_subsingleton_away, MatrixModCat.mem_toModuleCatObj, starProjection_bot, Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, linearIndependent_fin_succ', IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem, LinearIndepOn.notMem_span_of_insert, exteriorPower.ιMulti_family_eq_coe_comp, exteriorPower.pairingDual_ιMulti_ιMulti, mem_skewAdjointMatricesLieSubalgebra, groupHomology.H2π_eq_iff, span_eq, mulRightMap_eq_mulMap_comp, le_isotypicComponent, LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace, ZLattice.covolume.tendsto_card_le_div', LinearMap.mem_range_self, isNoetherian_submodule', mem_inf, exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, rank_span_finset_le, PointedCone.coe_closure, groupHomology.H1AddEquivOfIsTrivial_single, Int.absNorm_under_mem, isLinearTopology_iff_hasBasis_ideal, PadicInt.zmodRepr_spec, groupCohomology.mem_cocycles₁_iff, coe_iInf, MvPolynomial.monomial_mem_coeffsIn, Ideal.span_eq, IsAdjoinRoot.repr_zero_mem_span, coe_subset_nonunits, MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, Ideal.Filtration.submodule_span_single, finrank_map_le, finrank_span_eq_card, starProjection_unit_singleton, groupCohomology.mem_cocycles₂_of_comp_eq_d₁₂, LinearIsometryEquiv.ofTop_apply, prodComm_trans_prodEquivOfIsCompl, groupHomology.isoCycles₂_hom_comp_i_apply, LinearPMap.fst_apply, PointedCone.tmul_subset_maxTensorProduct, Ideal.span_singleton_le_iff_mem, DirectSum.decompose_algebraMap, LinearMap.compLeftInverse_apply_of_bdd, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, RootPairing.zero_le_posForm, finrank_eq_zero, Module.length_bot, CliffordAlgebra.ι_mul_ι_mem_evenOdd_zero, PowerBasis.mem_span_pow, rTensorOne_tmul, ContinuousLinearEquiv.toSpanNonzeroSingleton_symm_apply, annihilator_top_inter_nonZeroDivisors, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, reflection_sub, exists_fun_fin_finrank_span_eq, groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply, Ideal.hasBasis_nhds_zero_adic, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, AffineSubspace.coe_vadd, Ideal.add_eq_one_iff, Ideal.instIsTorsionFreeSubtypeMemSubmodule, Module.Finite.of_isComplemented_domain, Polynomial.degreeLT.addLinearEquiv_apply', affineIndependent_iff_le_finrank_vectorSpan, Subspace.quotAnnihilatorEquiv_apply, skewAdjointPart_comp_subtype_selfAdjoint, groupCohomology.isoCocycles₁_inv_comp_iCocycles, unitsToPic_apply, Affine.Simplex.circumcenter_restrict, Ideal.mem_span_singleton_sup, Module.isTorsionBySet_iff_subseteq_ker_lsmul, instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy, coe_zero, AffineMap.restrict.injective, FractionalIdeal.exists_mem_algebraMap_eq, Module.End.mem_genEigenspace_top, coe_mulMap_comp_eq, Affine.Simplex.height_restrict, exteriorPower.oneEquiv_symm_apply, ModuleCat.imageIsoRange_inv_image_ι, instModuleFinite_of_discrete_submodule, LinearMap.finrank_range_le, isIdempotentElemEquiv_apply_coe, mem_toAddSubgroup, TensorProduct.exists_finite_submodule_left_of_finite', LinearPMap.add_apply, EuclideanGeometry.orthogonalProjection_affineSpan_singleton, Rat.HeightOneSpectrum.natGenerator_dvd_iff, LinearEquiv.submoduleMap_apply, ContinuousLinearEquiv.ofSubmodule'_apply, Module.Flat.iff_lTensor_injective, groupHomology.cyclesMap_comp_isoCycles₂_hom_assoc, Module.Basis.mem_span_image, LieModule.Cohomology.mem_twoCocycle_iff, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_notMem, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom, exists_isInternal_prime_power_torsion_of_pid, PeriodPair.weierstrassP_add_coe, Ideal.natCast_mem_of_charP_quotient, Ideal.Quotient.eq_zero_iff_mem, closure_subset_span, exteriorPower.map_comp_ιMulti, AffineSubspace.subtype_injective, PrimeSpectrum.isClosed_iff_zeroLocus_ideal, groupCohomology.coboundariesOfIsCoboundary₁_coe, Module.End.isFinitelySemisimple_iff', AffineSubspace.subtype_linear, Ideal.basisSpanSingleton_apply, TensorProduct.quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk, colon_eq_top_iff_subset, PeriodPair.instProperSpaceSubtypeComplexMemSubmoduleIntLattice, coe_inner, orthogonalProjection_apply_eq_linearProjOfIsCompl, ZSpan.span_top, TensorProduct.tensorQuotientEquiv_apply_mk_tmul, isSMulRegular_quotient_iff_mem_of_smul_mem, IsLattice.span_eq_top, ExteriorAlgebra.instGradedMonoidNatSubmoduleExteriorPower, Algebra.Presentation.relation_mem_ker, TensorProduct.exists_finite_submodule_of_finite, MvPolynomial.mem_map_C_iff, MeasureTheory.condExpL2_indicator_of_measurable, HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented_self, derivationToSquareZeroEquivLift_symm_apply_apply_coe, GradedTensorProduct.mulHom_apply, EuclideanGeometry.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq, MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictDegreeOfFinite, exists_mem_ne_zero_of_ne_bot, closure_coe_iSup_map_single, Ideal.isCoprime_tfae, MvPolynomial.mem_restrictSupport_iff, LinearMap.eqOn_span_iff, AddMonoidAlgebra.GradesBy.decompose_single, AffineSubspace.topEquiv_symm_apply_coe, coe_isComplEquivProj_apply, AffineSubspace.isometryEquivMap.coe_apply, smul_mem_iff_of_isUnit, Subbimodule.coe_toSubbimoduleInt, prodEquivOfIsCompl_symm_apply_left, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem, linearIndependent_fin_snoc, sndL_comp_coe_orthogonalDecomposition, RootPairing.PolarizationIn_apply, injective_subtype, LinearIndepOn.mem_span_iff_id, linearProjOfIsCompl_isCompl_projection, stereographic_neg_apply, LinearMap.mem_ker, quotientEquivOfIsCompl_apply_mk_coe, InnerProductSpace.gramSchmidt_def', MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp, LinearMap.coe_domRestrict, NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite, Ideal.exists_forall_sub_mem_ideal, localized'_eq_span, linearProjOfIsCompl_comp_subtype, IsSemisimpleModule.sSup_simples_le, Representation.averageMap_invariant, AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact, rank_eq_zero, IsLattice.finrank_of_pi, Polynomial.degreeLT.addLinearEquiv_symm_apply_inl, coe_subtypeₗᵢ, Polynomial.degreeLT.addLinearEquiv_symm_apply_inr_basis, LinearMap.IsSymmetric.directSum_isInternal_of_commute, MvPolynomial.weightedHomogeneousComponent_directSum, IsSemisimpleModule.exists_simple_submodule, HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented_fst, smul_closure_subset, MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace, AddMonoidAlgebra.mem_grade_iff', Ideal.coe_toTwoSided, ZSpan.exist_unique_vadd_mem_fundamentalDomain, groupHomology.mapCycles₂_id_comp_assoc, groupHomology.π_comp_H1Iso_hom_apply, Rep.coindIso_inv_hom_hom, Finsupp.restrictDom_comp_subtype, Module.Finite.span_singleton, span_eq_iUnion_nat, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, Module.isTorsionBySet_iff_is_torsion_by_span, PointedCone.tmul_subset_minTensorProduct, rTensor_mkQ, map_le_isotypicComponent, Collinear.finiteDimensional_vectorSpan, Polynomial.Monic.leadingCoeff_notMem, Valuation.Integers.maximalIdeal_eq_setOf_le_v_algebraMap, groupCohomology.map_id_comp_H0Iso_hom_apply, groupCohomology.cocycles₁_map_mul_of_isTrivial, exteriorPower.pairingDual_apply_apply_eq_one, Algebra.IsSmoothAt.exists_notMem_smooth, groupCohomology.subtype_comp_d₀₁_assoc, complete_of_finiteDimensional, Module.Flat.tensorProduct_mapIncl_injective_of_left, imaginaryPart_comp_subtype_selfAdjoint, iSupIndep.linearEquiv_apply, Localization.exists_awayMap_bijective_of_residueField_surjective, groupHomology.toCycles_comp_isoCycles₂_hom, ContinuousLinearEquiv.coord_toSpanNonzeroSingleton, HasRankNullity.rank_quotient_add_rank, groupCohomology.map_id_comp_H0Iso_hom, convex, Module.Flat.iff_lTensor_injectiveₛ, groupHomology.cyclesMap_comp_isoCycles₂_hom_apply, coe_sub, mem_smul_pointwise_iff_exists, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc_apply, torsionBy.mk_ideal_smul, Span.finsupp_linearCombination_repr, SetLike.algebraMap_mem_graded, mem_span_iff_of_fintype, EuclideanGeometry.eq_or_eq_reflection_of_dist_eq, Affine.Simplex.incenter_restrict, PrimeSpectrum.zeroLocus_bot, LinearPMap.mem_graph_iff, isClosed_orthogonal, IsLattice.rank_of_pi, mem_vectorSpan_pair_rev, groupHomology.mapCycles₁_id_comp, SetLike.GradeZero.coe_algebraMap, InnerProductGeometry.angle_eq_angle_add_angle_iff, coe_torsionBySet, mem_dualCoannihilator, IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite, PointedCone.subset_span, toENat_rank_span_set, iSup_eq_span, CliffordAlgebra.reverse_mem_evenOdd_iff, LieModule.Cohomology.add_apply_apply, groupCohomology.cocycles₁IsoOfIsTrivial_inv_hom_apply_coe, EuclideanGeometry.orthogonalProjection_vadd_smul_vsub_orthogonalProjection, torsionBySet_torsionBySet_eq_top, MeasureTheory.condExpL1CLM_lpMeas, rTensorOne_tmul_one, toLinearMap_prodEquivOfIsCompl_symm, Ideal.Quotient.eq, Ideal.IsHomogeneous.isPrime_iff, PeriodPair.latticeBasis_one, Subbimodule.coe_toSubbimoduleNat, ClosedSubmodule.mem_orthogonal_toSubmodule_iff, diffToIdealOfQuotientCompEq_apply, finrank_eq_rank, ZLattice.covolume_eq_det_mul_measureReal, Ideal.eq_jacobson_iff_notMem, LinearPMap.map_neg, Subspace.finrank_add_finrank_dualCoannihilator_eq, MvPolynomial.mem_weightedHomogeneousSubmodule, RingHom.surjectiveOnStalks_iff_forall_maximal', mem_span_singleton_mul, groupCohomology.cocyclesOfIsMulCocycle₂_coe, Ideal.IsPrime.multiset_prod_mem_iff_exists_mem, Function.Exact.linearMap_rangeRestrict, PeriodPair.weierstrassP_sub_coe, Affine.Simplex.orthogonalProjectionSpan_faceOpposite_eq_point_rev, Module.Finite.range, sInf_coe, ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite, TensorProduct.forall_vanishesTrivially_iff_forall_rTensor_injective, Valued.integer.coe_span_singleton_eq_closedBall, Ideal.IsPrime.mem_or_mem_of_mul_eq_zero, PadicInt.mem_span_pow_iff_le_valuation, LinearIndependent.linearCombinationEquiv_symm_apply, equivSubtypeMap_apply, ClosedComplemented.isClosed, ZSpan.isAddFundamentalDomain, Algebra.Extension.Hom.mapKer_apply_coe, NumberField.discr_mem_differentIdeal, EuclideanGeometry.dist_orthogonalProjection_eq_infNndist, isIdempotentElemEquiv_symm_apply_coe, AddSubgroup.coe_toZModSubmodule, mem_skewAdjointMatricesSubmodule, MvPolynomial.mem_coeffsIn, FiniteDimensional.finiteDimensional_submodule, PrimeSpectrum.range_comap_snd, abs_signedDist_eq_dist_iff_vsub_mem_span, groupCohomology.coboundariesOfIsMulCoboundary₁_coe, Algebra.Extension.contangentEquiv_tmul, IsLinearTopology.hasBasis_submodule', coe_inf, NumberField.Units.instDiscrete_unitLattice, LinearMap.IsSymmetric.direct_sum_isInternal, det_reflection, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, LinearPMap.map_sub, LinearMap.quotKerEquivRange_apply_mk, Algebra.Generators.cMulXSubOneCotangent_eq, rank_span_le, FractionalIdeal.coeToSet_coeToSubmodule, NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, ValuationSubring.coe_mem_nonunits_iff, Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval, ContinuousLinearEquiv.toSpanNonzeroSingleton_coord, Ideal.toCotangent_apply, inner_orthogonalProjection_eq_of_mem_left, LieAlgebra.InvariantForm.restrict_orthogonal_nondegenerate, rank_submodule_eq_one_iff, Module.End.mem_iInf_maxGenEigenspace_iff, groupHomology.isoCycles₁_hom_comp_i_apply, Polynomial.isEisensteinAt_iff, starConvex, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_mem, AffineMap.restrict.surjective, Affine.Simplex.inradius_restrict, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, Finsupp.supportedEquivFinsupp_symm_apply_coe_support_val, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, PointedCone.ext_iff, AffineSubspace.subtypeₐᵢ_linear, ZLattice.exists_forall_abs_repr_le_norm, linearIndependent_fin_succ, AffineMap.restrict.coe_apply, linearMap_eq_iff_of_eq_span, CategoryTheory.ShortComplex.exact_iff_surjective_moduleCatToCycles, Algebra.IsEtaleAt.exists_isStandardEtale, ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal, PrimeSpectrum.zeroLocus_mul, RootPairing.prod_rootFormIn_smul_coroot_mem_range_PolarizationIn, ModuleCat.imageIsoRange_inv_image_ι_assoc, Ideal.eq_top_iff_one, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, IsSemisimpleModule.sSup_simples_eq_top, groupCohomology.H1π_eq_zero_iff, AddMonoidAlgebra.single_mem_grade, PeriodPair.hasSum_weierstrassP, mem_right_iff_eq_zero_of_disjoint, ProjectiveSpectrum.zeroLocus_bot, PeriodPair.coeff_weierstrassPSeries, AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine, Algebra.Extension.h1Cotangentι_ext_iff, PeriodPair.isOpen_compl_lattice_diff, Ideal.coe_comap, Ideal.toCotangent_eq_zero, exteriorPower.ιMulti_family_span_of_span, NumberField.fractionalIdeal_rank, toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl, Ideal.mul_unit_mem_iff_mem, MvPolynomial.decomposition.decompose'_apply, groupCohomology.coboundaries₁.val_eq_coe, PeriodPair.derivWeierstrassP_coe, mulRightMap_apply, MvPolynomial.mem_degreesLE, LieHom.quotKerEquivRange_invFun, Module.isTorsionBy_iff_mem_ker_lsmul, IsLattice.free, LinearPMap.map_smul, Module.injOn_dualMap_subtype_span_range_range, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_apply, mem_affineSpan_iff_exists, map₂_le, LieSubalgebra.coe_ofLe, Real.Convex.dimH_eq_finrank_vectorSpan, Ideal.zero_mem, nontrivial_span_singleton, quotientEquivOfIsCompl_symm_apply, Ideal.isCoprime_iff_exists, Ideal.mem_primeCompl_iff, MvPolynomial.monomial_mem_restrictSupport, RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff, GradedTensorProduct.auxEquiv_tmul, Ideal.cotangentEquivIdeal_apply, ModuleCat.kernelIsoKer_hom_ker_subtype, exteriorPower.map_injective_field, groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁, groupHomology.H1ToTensorOfIsTrivial_H1π_single, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc_apply, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangent, Algebra.Extension.H1Cotangent.val_add, LinearEquiv.coe_ofEq_apply, Polynomial.degreeLT.addLinearEquiv_symm_apply, coord_norm', RootPairing.algebraMap_posRootForm_posForm, PadicInt.norm_le_pow_iff_mem_span_pow, Ideal.sum_pow_mem_span_pow, Ideal.apply_mem_of_equiv_iff, coe_torsionBy, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, Basis.mem_ideal_iff', groupCohomology.cocyclesMk₁_eq, Algebra.idealMap_isLocalizedModule, IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff, PrimeSpectrum.closure_image_comap_zeroLocus, RingHom.one_notMem_ker, DirectSum.decomposeLinearEquiv_apply, Subalgebra.finiteDimensional_toSubmodule, exteriorPower.alternatingMapLinearEquiv_comp, collinear_iff_rank_le_one, Finsupp.linearCombination_restrict, Algebra.Extension.H1Cotangent.val_smul, MvPolynomial.mem_homogeneousSubmodule, topologicalClosure_coe, smul_mem_iff', groupHomology.cyclesOfIsCycle₁_coe, LinearEquiv.ofSubmodule'_toLinearMap, finrank_top, DirectSum.decomposeLinearEquiv_symm_comp_lof, exteriorPower.basis_coord, FractionalIdeal.mem_span_mul_finite_of_mem_mul, ClosedSubmodule.mem_orthogonal_iff, EuclideanGeometry.orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem, LinearIndependent.repr_range, range_deriv_subset_closure_span_image, Algebra.Extension.Cotangent.mk_eq_mk_iff_sub_mem, IsDedekindDomain.HeightOneSpectrum.intAdicAbv_eq_one_iff, Rep.quotientToInvariantsFunctor_obj_V, Polynomial.mem_iff_annIdealGenerator_dvd, ZLattice.covolume.tendsto_card_div_pow', IsSemisimpleModule.exists_end_ringEquiv, Module.End.mem_eigenspace_iff, Module.isPrincipal_submodule_iff, Ideal.constr_basisSpanSingleton, Polynomial.coeff_divModByMonicAux_mem_span_pow_mul_span, Function.Exact.iff_linearMap_rangeRestrict, Module.isTorsionBySet_annihilator_top, Localization.exists_awayMap_injective_of_localRingHom_injective, Ideal.apply_coe_mem_map, RootPairing.range_polarizationIn, RootPairing.restrictScalars_coe_root, mem_span_range_iff_exists_fun, exteriorPower.presentation_relation, PrimeSpectrum.closure_singleton, Ideal.mem_map_C_iff, mem_selfAdjointMatricesSubmodule, mulMap_one_left_eq, LinearMap.finrank_maxGenEigenspace, groupHomology.d₂₁_apply_mem_cycles₁, stereographic_target, starProjection_apply_mem, coe_set_mk, LieModule.Cohomology.smul_apply_apply, groupCohomology.coboundariesToCocycles₂_apply, EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq, AddMonoidAlgebra.gradeBy.gradedMonoid, MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite, quotDualCoannihilatorToDual_injective, Affine.Simplex.centroid_restrict, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_apply, groupHomology.cyclesMap_comp_isoCycles₁_hom_apply, Module.AEval.mem_mapSubmodule_symm_apply, UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime, mem_toAddSubmonoid, groupHomology.toCycles_comp_isoCycles₂_hom_apply, groupCohomology.cocyclesOfIsMulCocycle₁_coe, LinearPMap.coprod_apply, TensorProduct.exists_finite_submodule_of_setFinite', groupCohomology.H2π_eq_zero_iff, MvPolynomial.DirectSum.coeLinearMap_eq_finsum, LinearIsometryEquiv.submoduleMap_symm_apply_coe, LinearMap.disjoint_ker_iff_injOn, LieModule.Cohomology.instLinearMapClassSubtypeLinearMapIdMemSubmoduleTwoCochain, Subspace.dualRestrict_surjective, Coplanar.finiteDimensional_vectorSpan, groupCohomology.mapCocycles₁_comp_i_assoc, groupCohomology.cocycles₁.val_eq_coe, Ideal.mem_iInf, PointedCone.mem_span_set, AddSubgroup.coe_toIntSubmodule, ker_subtypeL, LinearMap.kerComplementEquivRange_symm_apply, mem_orthogonal, groupCohomology.H1π_comp_map_apply, StrongDual.mem_polarSubmodule, ProjectiveSpectrum.gc_ideal, LinearMap.lift_rank_range_add_rank_ker, groupCohomology.cocycles₁_map_one, TensorAlgebra.GradedAlgebra.ι_apply, MeasureTheory.integrable_condExpL2_of_isFiniteMeasure, PeriodPair.latticeEquiv_symm_apply, HahnEmbedding.ArchimedeanStrata.isInternal_stratum', groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, Ideal.not_isPrime_iff, EuclideanGeometry.dist_orthogonalProjection_eq_infDist, exteriorPower.instFinite, EuclideanGeometry.orthogonalProjection_mem, LinearEquiv.coord_self, Ideal.subset_union_prime_finite, isCentralScalar, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept, exteriorPower.alternatingMapToDual_apply_ιMulti, groupCohomology.π_comp_H2Iso_hom_assoc, Affine.Simplex.orthogonalProjectionSpan_restrict, nonempty, isArtinian_submodule', Representation.Coinvariants.mk_eq_zero, isClosed_nullSubmodule, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, KaehlerDifferential.D_tensorProductTo, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, Ring.KrullDimLE.isNilpotent_iff_mem_maximalIdeal, nat_power_gradedMonoid, Ideal.mem_span, LinearEquiv.ofEq_symm, IsSemisimpleModule.exists_end_algEquiv, Ideal.mem_span_range_iff_exists_fun, IsCompl.projection_apply_eq_zero_iff, MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree, mulMap_eq_mul'_comp_mapIncl, DirectSum.decomposeLinearEquiv_symm_apply, LinearEquiv.ofLeftInverse_apply, setBasisOfTopLeSpanOfCardEqFinrank_repr_apply, weightedVSub_mem_vectorSpan, liftOfDerivationToSquareZero_apply, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, LieSubmodule.coe_lieSpan_submodule_eq_iff, Algebra.Extension.Cotangent.mk_surjective, Algebra.exists_formallyUnramified_of_isUnramifiedAt, Affine.Simplex.setInterior_restrict, isLinearTopology_iff_hasBasis_open_ideal, AffineSubspace.finiteDimensional_sup, Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_aeval_zero_of_monic_mem_map, IsLocalization.smul_mem_iff, PrimeSpectrum.gc_set, mem_pNilradical, IsLocalization.orderIsoOfPrime_symm_apply_coe, LinearIndepOn.mem_span_iff, AddMonoidAlgebra.mem_grade_iff, rank_add_le_rank_add_rank, TwoSidedIdeal.mem_asIdeal, RootPairing.RootPositiveForm.isSymm_posForm, FractionalIdeal.isNoetherian_iff, mem_smul_top_iff, ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom, ZLattice.covolume.tendsto_card_le_div, ProjectiveSpectrum.zeroLocus_anti_mono_ideal, DirectSum.decomposeAlgEquiv_apply, torsionBySet_span_singleton_eq, AffineIndependent.finrank_vectorSpan, AddMonoidAlgebra.grade.decompose_single, IsCompl.projection_apply, mem_annihilator_span, Module.Basis.self_mem_flag_iff, InnerProductSpace.mem_span_gramSchmidt, mulLeftMap_eq_mulMap_comp, Representation.subrepresentation_apply, groupHomology.mapCycles₂_hom, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, MeasureTheory.integrable_condExpL2_indicator, rank_quotient_add_rank_le, LieAlgebra.Extension.d₁₂_oneCochainOfTwoSplitting, LinearMap.mem_selfAdjointSubmodule, groupHomology.isoCycles₂_inv_comp_iCycles_apply, LinearMap.finrank_range_dualMap_eq_finrank_range, Subbimodule.coe_toSubmodule, Affine.Simplex.excenterWeights_restrict, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff, AffineEquiv.ofEq_symm, Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_root_of_monic_mem, nontrivial_iff_ne_bot, image_span_subset, LinearIndepOn.notMem_span_iff_id, Algebra.Extension.Hom.subToKer_apply_coe, reflection_eq_self_iff, stereographic_source, ModuleCat.kernelIsoKer_hom_ker_subtype_apply, HasStrictFDerivAt.implicitToOpenPartialHomeomorph_self, Algebra.Generators.ofComp_kerCompPreimage, HahnEmbedding.ArchimedeanStrata.iSupIndep_stratum', LinearMap.IsProj.eq_conj_prod_map', IsIntegral.mem_span_pow, LinearEquiv.submoduleMap_symm_apply, IsHomogeneous.mem_iff, IsLocalization.disjoint_comap_iff, MvPolynomial.mem_restrictDegree_iff_sup, mem_span_pair, RootPairing.root_mem_submodule_iff_of_add_mem_invtSubmodule, Ideal.mem_inf, EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq, LinearMap.mem_range, groupHomology.cyclesMk₂_eq, LinearMap.BilinForm.finrank_orthogonal, Rep.coindVEquiv_apply_hom, mem_nullSubmodule_iff, mem_span_of_iInf_ker_le_ker, Polynomial.degreeLT.addLinearEquiv_symm_apply', LinearDisjoint.rank_le_one_of_flat_of_self, ContinuousLinearMap.projKerOfRightInverse_comp_inv, LinearEquiv.toSpanNonzeroSingleton_symm_apply_smul, Polynomial.coeff_mem_radical_span_coeff_of_dvd, IsZLattice.span_top, MonoidAlgebra.mem_ideal_span_of_image, Module.Basis.self_mem_span_image, instInvertibleSubtypeMemVal, AffineSubspace.linear_equivMapOfInjective, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_assoc, EuclideanGeometry.Sphere.IsTangentAt.eq_orthogonalProjection, Subbimodule.coe_toSubmodule', groupHomology.H1π_eq_zero_iff, Ideal.mem_iInf_smul_pow_eq_bot_iff, zero_mem, Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, MeasureTheory.MemLp.condExpL2_ae_eq_condExp', LinearMap.BilinForm.IsSymm.restrict, groupHomology.π_comp_H1Iso_hom_assoc, Affine.Simplex.median_restrict, isNilpotent_tensor_residueField_iff, Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset, toIsOrderedCancelAddMonoid, Ideal.rank_pow_quot_aux, traceDual_eq_span_map_traceDual_of_linearDisjoint, isNoetherian_of_fg_of_noetherian, LinearMap.range_liftBaseChange, groupHomology.H2π_comp_map, RootPairing.rootSpanMem_reflectionPerm_self, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_apply, coe_smul, Subspace.dualEquivDual_def, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, coe_span_eq_span_of_surjective, groupCohomology.cocycles₂.val_eq_coe, affineSpan_coe_preimage_eq_top, mem_one, TensorProduct.quotientTensorEquiv_apply_tmul_mk, exists_finset_span_eq_linearIndepOn, exteriorPower.zeroEquiv_ιMulti, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, smul_vsub_rev_mem_vectorSpan_pair, LinearPMap.mem_graph_iff', reflection_bot, LinearMap.surjective_comp_linearProjOfIsCompl, LinearMap.exact_subtype_ker_map, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff, HasStrictFDerivAt.implicitToOpenPartialHomeomorph_fst, Algebra.Extension.H1Cotangent.map_apply_coe, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, PeriodPair.analyticOnNhd_derivWeierstrassP, mulMap'_surjective, MvPowerSeries.coe_hasEvalIdeal, subtypeL_apply, AffineSubspace.coe_direction_eq_vsub_set_left, finrank_span_eq_finrank_span, restrictScalars_mem, instNonUnitalSubringClassIdeal, aeval_derivative_mem_differentIdeal, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, Module.isTorsionBySet_quotient_iff, mem_orthogonalBilin_iff, mem_smul_span, groupHomology.H1π_comp_map_assoc, Subspace.dualLift_rightInverse, Representation.Coinvariants.mk_eq_iff, Ideal.natAbs_det_equiv, LinearMap.map_coe_ker, torsion_gc, EuclideanGeometry.reflection_eq_iff_orthogonalProjection_eq, IsPrincipal.generator_mem, finrank_map_subtype_eq, groupHomology.instEpiModuleCatH1π, coe_dualAnnihilator_span, HasStrictFDerivAt.implicitToOpenPartialHomeomorph_apply_ker, ker_orthogonalProjection, NumberField.mem_span_integralBasis, Affine.Simplex.closedInterior_restrict, ClosedSubmodule.mem_mk, mem_carrier, groupCohomology.isoCocycles₂_inv_comp_iCocycles, MeasureTheory.lpTrimToLpMeas_ae_eq, AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty, LinearMap.ofIsCompl_add, LinearEquiv.ofSubmodule'_apply, starProjection_orthogonalComplement_singleton_eq_zero, FG.directedSystem, mem_span_of_mem, EuclideanGeometry.orthogonalProjection_orthogonalProjection, exteriorPower.map_injective, vectorSpan_add_self, Ideal.rank_pow_quot, Ideal.subtype_isoBaseOfIsPrincipal_eq_mul, MvPolynomial.mem_coeffsIn_iff_coeffs_subset, mem_iSup_finset_iff_exists_sum, eq_top_iff_forall_basis_mem, EuclideanGeometry.orthogonalProjection_vsub_mem_direction, exteriorPower.basis_repr_apply, iSup_eq_span', HasOrthogonalProjection.exists_orthogonal, mk_quotientEquivOfIsCompl_apply, smul_mem_iff, groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂, MvPolynomial.weightedDecomposition.decompose'_eq, prodEquivOfIsCompl_symm_apply_right, coe_mapIic_apply, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_symm_apply, submoduleOf_eq_top, Subspace.dualCopairing_nondegenerate, exteriorPower.presentation_R, ProjectiveSpectrum.ideal_le_vanishingIdeal_zeroLocus, restrictScalars.isScalarTower, mem_span, pow_eq_span_pow_set, finiteDimensional_direction_affineSpan_image_of_finite, groupHomology.instEpiModuleCatH2π, ContinuousLinearEquiv.submoduleMap_symm_apply, NumberField.mem_span_basisOfFractionalIdeal, exists_isInternal_prime_power_torsion, LinearIndepOn.image_subset_span_image_extend, Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq, Subbimodule.coe_baseChange, LinearMap.BilinForm.mem_orthogonal_iff, Polynomial.mem_ker_modByMonic, mem_vectorSpan_pair, AlgebraicGeometry.Spec.coe_toTop_map_hom_apply_asIdeal, IsArtinianRing.exists_not_mem_forall_mem_of_ne, AffineSubspace.topEquiv_apply, Basis.mem_ideal_iff, LinearEquiv.ofTop_symm_apply, Finsupp.mem_span_range_iff_exists_finsupp, groupCohomology.cocyclesMk₂_eq, LinearIsometry.completeSpace_map, GradedTensorProduct.tmul_coe_mul_zero_coe_tmul, Affine.Simplex.mongePoint_restrict, rank_span_of_finset, coe_smul_of_tower, PeriodPair.instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice, MvPolynomial.coeffsIn_eq_span_monomial, finrank_mono, mulLeftMap_apply_single, Finsupp.single_mem_span_single, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_subset_zeroLocus, ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl, support_of_supportDim_eq_zero, EuclideanGeometry.hasFDerivAt_inversion, mem_coeSubmodule_conductor, mem_isotypicComponents_iff, LinearIndependent.repr_ker, groupHomology.H1π_comp_map, Affine.Simplex.eulerPoint_restrict, finrank_add_le_finrank_add_finrank, groupHomology.d₃₂_apply_mem_cycles₂, toLinearPMap_apply_aux, OrthonormalBasis.span_apply, Ideal.mem_quotient_iff_mem_sup, Ideal.mem_torsionOf_iff, le_div_iff, EuclideanGeometry.vsub_orthogonalProjection_mem_direction, span_sSup', mulMap_map_comp_eq, mem_span_triple, MeasureTheory.Measure.addHaar_submodule, GradedTensorProduct.comm_coe_tmul_coe, mem_torsionBy_iff, Module.Basis.flag_le_iff, instCompleteSpaceSubtypeMemSubmoduleOfIsClosedCoe, Valuation.Integers.isPrincipal_iff_exists_eq_setOf_valuation_le, Module.Flat.iff_lift_lsmul_comp_subtype_injective, ContinuousMap.adjoin_id_eq_span_one_add, ClosedSubmodule.instCanLiftSubmoduleToSubmoduleIsClosedCoe, AffineSubspace.coe_inclusion_apply, Algebra.exists_etale_of_isEtaleAt, Ideal.range_finsuppTotal, lt_sup_iff_notMem, groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply, Algebra.exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top, Affine.Simplex.ExcenterExists.touchpoint_restrict, AffineSubspace.signedInfDist_singleton, groupHomology.boundariesOfIsBoundary₂_coe, Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection, Module.Finite.top, biUnion_associatedPrimes_eq_compl_nonZeroDivisors, IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite, finrank_le_one_iff_isPrincipal, groupHomology.cyclesMk₁_eq, ne_bot_iff, Module.End.mem_invtSubmodule_iff_forall_mem_of_mem, FG.lTensor.directLimit_apply, IsCoprime.exists, LieSubmodule.coe_toSubmodule, finrank_span_eq_finrank, LinearMap.IsProj.codRestrict_ker, Collinear.finrank_le_one, AffineSubspace.vadd_mem_iff_mem_direction, Module.fgSystem.equiv_comp_of, HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented_apply, AddMonoidAlgebra.grade.isInternal, NumberField.FinitePlace.norm_eq_one_iff_notMem, groupHomology.mapCycles₂_comp_i_assoc, Ideal.unit_mul_mem_iff_mem, RootPairing.posRootForm_posForm_nondegenerate, isLinearTopology_iff_hasBasis_open_submodule, ArchimedeanClass.mem_closedBall_iff, Affine.Simplex.excenterWeightsUnnorm_restrict, groupCohomology.isoCocycles₁_hom_comp_i, Ideal.Quotient.mk_eq_mk_iff_sub_mem, AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet, range_inclusion, Module.Flat.instSubtypeMemSubmoduleSubmoduleAlgebra, MvPolynomial.HomogeneousSubmodule.gradedMonoid, ContinuousLinearMap.projKerOfRightInverse_apply_idem, mem_traceDual, coe_iSup_of_directed, LinearMap.domRestrict₂_apply, AffineSubspace.subtypeₐᵢ_linearIsometry, Ideal.coe_closure, LinearMap.IsIdempotentElem.mem_range_iff, Algebra.Extension.Hom.sub_aux, mul_subset_mul, PointedCone.mem_closure, Module.End.mem_genEigenspace_one, Polynomial.IsEisensteinAt.mem, Ideal.powQuotSuccInclusion_injective, LinearMap.IsProj.trace, IsLocalRing.CotangentSpace.map_eq_top_iff, LinearPMap.mem_graph, rank_range_of_injective, HahnEmbedding.ArchimedeanStrata.archimedean_stratum, Module.isTorsionBy_quotient_iff, basisOfPid_bot, IsLocalRing.isOpen_maximalIdeal_pow, exists_maximal_linearIndepOn, EuclideanGeometry.Sphere.IsTangent.isTangentAt, groupCohomology.mapCocycles₁_comp_i_apply, ZLattice.isAddFundamentalDomain, LinearMap.isClosed_or_dense_ker, Rep.coindMap_hom, isInternal_prime_power_torsion, LinearMap.restrict_smul_one, Module.End.mapsTo_maxGenEigenspace_of_comm, groupHomology.mapCycles₂_id_comp_apply, image2_subset_map₂, coe_eq_zero, coe_closure, LinearMap.range_domRestrict, Polynomial.det_taylorLinearEquiv, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end, Ideal.mem_map_iff_of_surjective, instIsTorsionFree, groupCohomology.cocycles₂_ext_iff, Algebra.Extension.h1Cotangentι_apply, coe_subtype, mulMap_comp_lTensor, LinearEquiv.rank_map_eq, isNoetherian_span_of_finite, mem_sInf, RootPairing.algebraMap_coroot'In_apply, smul_torsionBy, coe_neg, ContinuousLinearMap.IsPositive.orthogonalProjection_comp, LinearMap.linearEquiv_of_ne_zero, LinearMap.IsSymm.nondegenerate_restrict_of_isCompl_ker, smul_le, mem_localized₀, sup_eq_top_iff, dimH_orthogonalProjection_le, LinearMap.range_ofIsCompl, ClassGroup.exists_mk0_eq_mk0, RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic, instDiscreteTopologySubtypeMemSubmoduleIntComap, Module.End.mem_maxGenEigenspace, derivationOfSectionOfKerSqZero_apply_coe, torsionBy_isTorsionBy, span_span, Module.Finite.iff_fg, groupHomology.H2π_comp_map_apply, adjoint_orthogonalProjection, lTensorOne_symm_apply, LinearMap.tensorEqLocus_tmul, exteriorPower.map_comp_ιMulti_family, MvPolynomial.mul_monomial_mem_coeffsIn, EuclideanGeometry.reflection_apply', mul_le, fg_top, AffineIsometryEquiv.ofEq_rfl, RootPairing.rootFormIn_self_smul_coroot, MvPolynomial.C_mem_pow_idealOfVars_iff, tensorToSpan_apply_tmul, Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe, exteriorPower.map_id, LinearMap.ofIsCompl_left_apply, EuclideanGeometry.oangle_self_orthogonalProjection, nilpotent_iff_mem_prime, isCompl_comap_subtype_of_isCompl_of_le, le_isotypicComponent_iff, Projectivization.instFiniteDimensionalSubtypeMemSubmoduleSubmodule, LinearMap.ker_le_iff, LieModule.Cohomology.twoCochain_val_apply, Algebra.mem_ideal_map_adjoin, Module.Finite.of_fg, image_specComap_zeroLocus_eq_zeroLocus_comap, HasStrictFDerivAt.mem_implicitToPartialHomeomorphOfComplemented_source, AlgebraicGeometry.Scheme.zeroLocus_span, Ideal.nonempty_inter_nonZeroDivisors_of_faithfulSMul, LinearIsometry.strictConvexSpace_range_iff, linearIndependent_iff_notMem_span, DividedPowers.SubDPIdeal.memCarrier, mem_orthogonal_singleton_iff_inner_left, groupCohomology.coboundaries₁_ext_iff, fg_iff_finiteDimensional, iSupIndep_iff_dfinsupp_lsum_injective, mem_adjoint_iff, MvPolynomial.weightedHomogeneousComponent_mem, span_biUnion, Finsupp.supportedEquivFinsupp_symm_apply_coe, span_singleton_eq_range, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff, Ideal.disjoint_primeCompl_of_liesOver, exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul, LinearEquiv.toSpanNonzeroSingleton_one, lTensorOne'_one_tmul, Module.Basis.self_mem_flag, Ideal.IsPrime.exists_mem_prime_of_ne_bot, Ideal.colon_span, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_K, LinearMap.mem_graph_iff, LinearMap.coe_quotientInfToSupQuotient, Subspace.dualLift_injective, Algebra.Generators.cotangentRestrict_mk, MatrixModCat.toModuleCat_map, Polynomial.toMatrix_sylvesterMap, TensorProduct.exists_finite_submodule_right_of_finite, Finsupp.supportedEquivFinsupp_apply_support_val, LinearIsometryEquiv.reflections_generate_dim, GradedAlgebra.proj_apply, Ideal.coe_piOrderIso_symm_apply, FractionalIdeal.mem_coe, Irreducible.maximalIdeal_eq_closedBall, AffineEquiv.coe_ofEq_apply, PrimeSpectrum.coe_vanishingIdeal, finiteDimensional_bot, ContinuousLinearMap.exist_extension_of_finiteDimensional_range, span_inter, groupCohomology.π_comp_H2Iso_hom_apply, LinearPMap.mkSpanSingleton_apply, PeriodPair.hasSum_weierstrassPExcept, MeasureTheory.hausdorffMeasure_orthogonalProjection_le, small_span, coe_span_eq_self, CliffordAlgebra.even.lift.aux_apply, AffineSubspace.mem_direction_iff_eq_vsub_right, norm_coe, exists_lieSubalgebra_coe_eq_iff, finrank_add_finrank_orthogonal, instIsSemisimpleModuleSubtypeMemSubmoduleValSetIsotypicComponents, AffineMap.restrict.linear, map_subtype_top, AddSubmonoid.coe_toNatSubmodule, mem_toConvexCone, exteriorPower.pairingDual_apply_apply_eq_one_zero, lipschitzWith_orthogonalProjection, Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range, DividedPowers.IsSubDPIdeal.dpow_eq, Ideal.mem_span_pair, TopModuleCat.kerι_apply, Ideal.isRadical_iff_pow_one_lt, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, exists_fg_le_subset_range_rTensor_inclusion, Ideal.exists_mem_pow_notMem_pow_succ, derivationToSquareZeroEquivLift_apply_coe_apply, orthogonalFamily_iff_pairwise, span_span_coe_preimage, AffineSubspace.coe_subtype, Module.support_eq_zeroLocus, Representation.coind_apply, mem_reesAlgebra_iff, groupHomology.isoCycles₁_hom_comp_i_assoc, ContinuousLinearEquiv.submoduleMap_apply, FractionalIdeal.abs_det_basis_change, ClosedComplemented.exists_submodule_equiv_prod, LinearMap.map_span_le, instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallHSMul, Rep.invariantsFunctor_map_hom, finrank_span_singleton, LieAlgebra.mem_corootSpace', Affine.Simplex.orthogonalProjectionSpan_reindex, Subalgebra.coe_toSubmodule, LinearPMap.vadd_apply, LinearMap.le_eqLocus, span_sup, liftOfDerivationToSquareZero_mk_apply', ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection, Module.Finite.map, rank_le_one_iff_isPrincipal, subalgebra_top_finrank_eq_submodule_top_finrank, Ideal.univ_eq_iUnion_image_add, PrimeSpectrum.basicOpen_le_basicOpen_iff, stereographic_apply, MeasureTheory.inner_condExpL2_eq_inner_fun, Ideal.mem_mul_span_singleton, ContinuousMap.mem_setOfIdeal, finite_dualAnnihilator_iff, linearProjOfIsCompl_comp_bijective_of_exact, RootPairing.RootPositiveForm.algebraMap_apply_eq_form_iff, MeasureTheory.mem_lpMeas_self, groupCohomology.π_comp_H1Iso_hom_apply, LinearMap.continuous_iff_isClosed_ker, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, ClassGroup.exists_min, LinearMap.rTensor_range, Module.Basis.SmithNormalForm.repr_comp_embedding_eq_smul, Representation.Coinvariants.mem_ker_of_eq, LinearIsometry.strictConvexSpace_range, PrimeSpectrum.mem_basicOpen, TensorProduct.exists_finite_submodule_right_of_finite', Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top, IsLocalRing.CotangentSpace.span_image_eq_top_iff, LinearEquiv.coord_apply_smul, LinearPMap.ext_iff, topologicalAddGroup, IsLocalRing.notMem_maximalIdeal, Ideal.isPrime_iff, RootPairing.restrictScalars_toLinearMap_apply_apply, LinearMap.finrank_maxGenEigenspace_zero_eq, fstL_comp_coe_orthogonalDecomposition, Polynomial.isWeaklyEisensteinAt_iff, RootPairing.finrank_corootSpan_eq, isPathConnected_compl_of_one_lt_codim, LinearMap.ofIsCompl_right_apply, NumberField.mixedEmbedding.fundamentalCone.preimage_of_IdealSetMap, Ideal.coe_prod, mem_span_set', Polynomial.sylvesterMap_apply_coe, vaddCommClass, Polynomial.degreeLT.addLinearEquiv_natAdd, linearDepOn_iffₛ, starProjection_minimal, PeriodPair.differentiableOn_weierstrassPExcept, EuclideanGeometry.orthogonalProjection_linear, PrimeSpectrum.subset_zeroLocus_vanishingIdeal, Valuation.mem_ltSubmodule_iff, ContinuousLinearEquiv.ofSubmodule'_symm_apply, pinGroup.involute_act_ι_mem_range_ι, Module.End.mem_genEigenspace_nat, inclusion_injective, Ideal.neg_mem_iff, mulMap_comp_map_inclusion, ContinuousLinearMap.completeSpace_ker, AffineSubspace.signedInfDist_def, PeriodPair.derivWeierstrassPExcept_add_coe, LinearMap.submoduleComap_surjective_of_surjective, IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top, starProjection_mem_subspace_eq_self, Ideal.Quotient.mk_eq_one_iff_sub_mem, exteriorPower.basis_repr, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter, angle_coe, exists_extension_norm_eq, MvPolynomial.mem_ideal_span_monomial_image_iff_dvd, NumberField.Units.unitLattice_rank, ProjectiveSpectrum.zeroLocus_sup_ideal, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_apply, IsSMulRegular.subsingleton_linearMap_iff, finrank_le, instNontrivialSubtypeMemSubmoduleValSetIsotypicComponents, groupHomology.π_comp_H2Iso_hom_apply, isArtinian_sup, lTensorOne_tmul, instIsSimpleModuleSubtypeMemSubmoduleValSetSetOfNonemptyLinearEquivId, coe_pi, LinearIndepOn.notMem_span_iff, PeriodPair.differentiableOn_weierstrassP, mem_colon_singleton, Module.Flat.iff_rTensor_injectiveₛ, LinearDisjoint.val_mulMap_tmul, FG.span, pow_subset_pow, Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle, Module.Dual.finrank_ker_add_one_of_ne_zero, Module.Finite.bot, Algebra.Extension.Hom.sub_tmul, exteriorPower.alternatingMapLinearEquiv_symm_apply, LinearIndependent.notMem_span_image, isLinearTopology_iff_hasBasis_submodule, ZLattice.normBound_spec, LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, groupHomology.mapCycles₁_hom, Module.isTorsionBySet_iff_subset_annihilator, instFreeSubtypeMemIdealOfFiniteOfIsTorsionFree, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π_hom, AddValuation.mem_supp_iff, mem_iSup_of_chain, LinearMap.exists_extend, isNoetherian_submodule_left, AffineSubspace.mem_mk', groupHomology.isoCycles₁_inv_comp_iCycles, Ideal.mem_span_insert, Ideal.isPrimary_iff, affineIndependent_iff_finrank_vectorSpan_eq, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, PointedCone.mem_comap, orthogonalProjectionFn_eq, mem_iSup_iff_exists_finset, ZSpan.discreteTopology_pi_basisFun, mul_eq_span_mul_set, RootPairing.finrank_rootSpanIn, Affine.Simplex.signedInfDist_affineCombination, Module.flat_iff, mem_colon, Polynomial.taylorLinearEquiv_symm, groupHomology.cyclesMap_comp_isoCycles₁_hom_assoc, EuclideanGeometry.angle_self_orthogonalProjection, exists_fg_le_eq_rTensor_subtype, LieSubalgebra.mem_mk_iff', FractionalIdeal.isNoetherian, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, groupHomology.coe_mapCycles₁, NumberField.Units.logEmbeddingEquiv_apply, ZLattice.covolume.tendsto_card_le_div'', Ideal.mem_radical_iff, groupHomology.toCycles_comp_isoCycles₁_hom, Polynomial.degreeLT.addLinearEquiv_symm_apply_inl_basis, iSup_eq_toSubmodule_range, TensorProduct.exists_finite_submodule_of_setFinite, TensorProduct.exists_finite_submodule_left_of_setFinite', exteriorPower.map_apply_ιMulti, MvPolynomial.one_coeffsIn, NumberField.basisOfFractionalIdeal_apply, PeriodPair.hasSum_sumInvPow, Module.Basis.ofZLatticeComap_repr_apply, signedDist_eq_dist_iff_vsub_mem_span, iSup_torsionBySet_ideal_eq_torsionBySet_iInf, LieSubalgebra.coe_lieSpan_submodule_eq_iff, HahnEmbedding.Partial.archimedeanClassMk_le_of_eval_eq, AffineSubspace.angle_coe, RootPairing.posRootForm_posForm_anisotropic, mem_sSup_iff_exists_finset, PrimeSpectrum.zeroLocus_inf, isScalarTower_of_section_of_ker_sqZero, LinearMap.IsSymmetric.LinearMap.IsSymmetric.directSum_isInternal_of_pairwise_commute, Finsupp.mem_ideal_span_range_iff_exists_finsupp, AddMonoidAlgebra.mem_span_support', finset_inf_coe, PrimeSpectrum.mem_vanishingIdeal, mem_finsetInf, groupHomology.mapCycles₂_comp_i_apply, Valuation.mem_leIdeal_iff, rank_quotient_add_rank_of_divisionRing, PowerSeries.mem_hasEvalIdeal_iff, torsionBySet_eq_torsionBySet_span, EuclideanGeometry.orthogonalProjection_eq_self_iff, linearIndepOn_insert, groupCohomology.cocyclesIso₀_hom_comp_f_apply, Ideal.subset_union_prime, groupHomology.boundariesToCycles₂_apply, Module.Finite.span_finset, Module.Finite.instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule_1, ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id, groupCohomology.subtype_comp_d₀₁, AddMonoidAlgebra.decomposeAux_single, EuclideanGeometry.reflection_subtype, subset_span, PeriodPair.periodic_weierstrassP, LinearPMap.mem_domain_iff_of_eq_graph, map_range_rTensor_subtype_lid, span_singleton_le_iff_mem, groupHomology.cyclesOfIsCycle₂_coe, LinearMap.det_eq_det_mul_det, isNoetherian_sup, FiniteDimensional.instSubtypeMemSubmoduleMap, eq_zero_of_bot_submodule, IsLinearTopology.hasBasis_ideal, ContinuousLinearEquiv.coord_norm', LinearEquiv.coe_ofTop_symm_apply, Ideal.coe_torsionOf, IsLattice.finite, mem_sup, groupHomology.isoCycles₂_hom_comp_i, LinearMap.injective_domRestrict_iff, groupHomology.π_comp_H1Iso_hom, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_H, LinearMap.mem_span_iff_bound, fstEquiv_symm_apply_coe, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc_apply, coe_set_smul, snd_orthogonalDecomposition_apply, groupHomology.isoCycles₂_inv_comp_iCycles, LinearMap.BilinForm.toLin_restrict_ker_eq_inf_orthogonal, asymptoticCone_submodule, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_apply, Module.Basis.ofZLatticeBasis_repr_apply, groupHomology.mkH1OfIsTrivial_apply, tendsto_card_div_pow_atTop_volume', CliffordAlgebra.ι_mem_evenOdd_one, fromModuleCatToModuleCatLinearEquiv_apply, Module.Finite.span_of_finite, notMem_of_ortho, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, top_coe, IsIsotypic.linearEquiv_finsupp, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, isCompact_of_fg, fromModuleCatToModuleCatLinearEquiv_symm_apply_coe, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom, PointedCone.mem_toConvexCone, LinearMap.surjective_rangeRestrict, AffineSubspace.isometryEquivMap.apply_symm_apply, coe_torsion_eq_annihilator_ne_bot, AffineSubspace.inclusion_rfl, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_of_mem, IsSemisimpleModule.eq_bot_or_exists_simple_le, linearProjOfIsCompl_range, Irreducible.maximalIdeal_pow_eq_closedBall_pow, NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule, instOrthogonalCompleteSpace, CharacterModule.intSpanEquivQuotAddOrderOf_apply_self, linearIndependent_option', LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter, linearIndepOn_id_insert, MvPolynomial.mem_vanishingIdeal_iff, MvPolynomial.mem_vanishingIdeal_singleton_iff, coe_mapAlgHom_apply, AlgHom.toKerIsLocalization_isLocalizedModule, CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_iff, FractionalIdeal.equivNum_apply, Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow, IsTopologicallyNilpotent.mem_topologicalNilradical_iff, Ideal.iUnion_minimalPrimes, exists_mem_sup, DividedPowers.isSubDPIdeal_inf_iff, ContinuousMap.mem_idealOfSet_compl_singleton, AddSubgroup.relIndex_eq_natAbs_det, isNoetherian_of_submodule_of_noetherian, coe_norm, orthogonalDecomposition_apply, Ideal.Quotient.quotient_ring_saturate, groupHomology.single_one_mem_boundaries₁, Ideal.relNorm_apply, map_comap_subtype, spanRank_top, AntilipschitzWith.completeSpace_range_clm, LinearIsometry.isComplete_map_iff', Finsupp.mem_span_image_iff_linearCombination, IsDedekindDomain.isOpen_of_ne_bot, ProjectiveSpectrum.zeroLocus_span, exteriorPower.map_comp, PeriodPair.mul_ω₁_add_mul_ω₂_mem_lattice, groupHomology.π_comp_H1Iso_inv_apply, NumberField.mixedEmbedding.fundamentalCone.mem_idealSet, Ideal.mem_pi, lift_rank_range_le, ZSpan.vadd_mem_fundamentalDomain, exteriorPower.ιMultiDual_apply_nondiag, MvPolynomial.mem_ideal_span_monomial_image, sSup_simples_eq_top_iff_isSemisimpleModule, Polynomial.taylor_mem_degreeLT, Ideal.mem_span_singleton_mul, Subrepresentation.mem_ofSubmodule_iff, AddMonoidAlgebra.decomposeAux_eq_decompose, HasStrictFDerivAt.mem_implicitToPartialHomeomorph_source, ValuationSubring.coe_primeSpectrumOrderEquiv_symm_apply_asIdeal, exteriorPower.presentation_var, GradedTensorProduct.tmul_algebraMap_mul_coe_tmul, ZSpan.fract_apply, groupCohomology.isoCocycles₂_hom_comp_i_apply, LinearIsometryEquiv.ofEq_rfl, LieAlgebra.mem_corootSpace, mulMap_op, LinearEquiv.ofEq_rfl, HasStrictFDerivAt.implicitToPartialHomeomorph_fst, HasStrictFDerivAt.mem_implicitToPartialHomeomorph_target, torsionBySet.mk_smul, EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal, AffineSubspace.vsub_right_mem_direction_iff_mem, isNoetherian_top_iff, Ideal.IsPrime.prod_mem_iff_exists_mem, LieModule.Cohomology.mem_twoCocycle_iff_of_trivial, HahnEmbedding.Partial.sSupFun_strictMono, MeasureTheory.lpMeasToLpTrim_ae_eq, orthogonal_eq_inter, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_apply, FG.small, MeasureTheory.eLpNorm_condExpL2_le, mem_sSup_of_directed, smul_vsub_mem_vectorSpan_pair, isPathConnected, finrank_vectorSpan_range_add_one_le, mem_annihilator_span_singleton, PointedCone.isClosed_dual, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc_apply, Module.Flat.tensorProduct_mapIncl_injective_of_right, ContinuousLinearEquiv.toSpanNonzeroSingleton_apply_coe, mem_span_set_iff_exists_finsupp_le_finrank, ContinuousLinearEquiv.coord_self, UniformOnFun.continuousSMul_submodule_of_image_bounded, isSMulRegular_on_submodule_iff_disjoint_ker_lsmul_submodule, RingHom.sub_mem_ker_iff, LinearMap.ofIsCompl_subtype_zero_eq, Derivation.liftKaehlerDifferential_apply, one_le, LinearEquiv.finrank_map_eq, groupHomology.cycles₁IsoOfIsTrivial_inv_apply, map_subtype_range_inclusion, finrank_bot, ContinuousLinearEquiv.coord_norm, existsUnique_add_of_isCompl, FiniteDimensional.subalgebra_toSubmodule, HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented_apply_ker, exteriorPower.map_surjective, KaehlerDifferential.DLinearMap_apply, Ideal.mem_span_singleton, MeasureTheory.lpMeasToLpTrim_smul, groupCohomology.coboundaries₂_ext_iff, NonUnitalSubalgebra.mem_toSubmodule, MvPolynomial.C_mem_coeffsIn, LinearPMap.mem_adjoint_domain_iff, IsLocalization.mem_coeSubmodule, vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan, CliffordAlgebra.GradedAlgebra.lift_ι_eq, AddSubgroup.mem_toZModSubmodule, linearProjOfIsCompl_ker, EuclideanGeometry.eq_orthogonalProjection_of_eq_subspace, groupCohomology.cocyclesOfIsCocycle₂_coe, LinearEquiv.lift_rank_map_eq, EuclideanGeometry.orthogonalProjection_apply, Module.Basis.extendOfIsLattice_apply, groupHomology.isoCycles₁_hom_comp_i, Ideal.exists_disjoint_powers_of_span_eq_top, mem_selfAdjointMatricesSubmodule', groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, Module.End.hasGenEigenvector_iff, torsion_isTorsion, Convex.semilinear_range, PeriodPair.analyticOnNhd_weierstrassPExcept, rank_span, norm_orthogonalProjection, AffineSubspace.signedInfDist_apply_self, EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection, PrimeSpectrum.zeroLocus_sup, EuclideanGeometry.orthogonalProjection_mem_orthogonal, ProjectiveSpectrum.zeroLocus_iSup_ideal, Polynomial.degreeLT.basisProd_natAdd, torsionBy_isInternal, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange, exteriorPower.presentation_G, mem_set_smul, GradedTensorProduct.tmul_coe_mul_algebraMap_tmul, groupCohomology.H1π_comp_map, lTensorOne_one_tmul, PointedCone.mem_positive, groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁, Module.End.mem_genEigenspace_zero, LinearMap.finrank_maxGenEigenspace_eq, LinearMap.IsProj.codRestrict_apply, lipschitzGroup.involute_act_ι_mem_range_ι, map_coe, ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id, LinearMap.BilinForm.toLin_restrict_range_dualCoannihilator_eq_orthogonal, LinearMap.nondegenerate_restrict_of_disjoint_orthogonal, LinearPMap.coe_vadd, AffineSubspace.mem_direction_iff_eq_vsub_left, span_range_eq_top_of_injective_of_rank_le, finrank_lt, rank_sup_add_rank_inf_eq, ZSpan.repr_floor_apply, PointedCone.mem_maxTensorProduct, MeasureTheory.condExpIndSMul_ae_eq_smul, rank_top, Module.fgSystem.instDirectedSystemSubtypeSubmoduleFGMemValCoeLinearMapId, isNoetherian_range, linearProjOfIsCompl_apply_eq_zero_iff, coplanar_iff_finrank_le_two, LinearMap.tensorKerEquiv_apply, Localization.exists_awayMap_bijective_of_localRingHom_bijective, WittVector.mem_span_p_iff_coeff_zero_eq_zero, Polynomial.mem_degreeLE, finite_sup, IsLocalization.mem_map_algebraMap_iff, mem_biSup_iff_exists_dfinsupp, exteriorPower.ιMulti_family_linearIndependent_ofBasis, MeasureTheory.lpMeas.ae_fin_strongly_measurable', Ideal.mem_span_insert', PrimeSpectrum.localization_comap_range, RingHom.ker_eq, IsLocalization.orderIsoOfPrime_apply_coe, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe, PointedCone.dual_flip_dual_dual_flip, groupCohomology.cocyclesMk₀_eq, EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self, range_subtype, coe_toSubMulAction, range_derivWithin_subset_closure_span_image, NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype, vsub_set_subset_vectorSpan, Ideal.ext_iff, ProperCone.mem_toPointedCone, subtype_injective, Set.MapsTo.submoduleSpan, mem_div_iff_smul_subset, dualRestrict_apply, LinearMap.BilinForm.finrank_add_finrank_orthogonal, smulMemClass, Ideal.mem_comap, Module.End.mem_genEigenspace, IsSemisimpleModule.exists_linearEquiv_dfinsupp, neg_coe, groupHomology.single_mem_cycles₂_iff, HasStrictFDerivAt.implicitFunctionOfComplemented_apply_image, IsPrincipal.mem_iff_generator_dvd, GradedAlgebra.mem_support_iff, finrank_quotient, Int.absNorm_under_eq_sInf, comapSubtypeEquivOfLe_apply_coe, Ideal.IsLocal.mem_jacobson_or_exists_inv, Ideal.algebraMap_residueField_eq_zero, RootPairing.RootPositiveForm.algebraMap_posForm, PrimeSpectrum.range_comap_fst, AmpleSet.of_one_lt_codim, ModuleCat.mono_as_hom'_subtype, Ideal.dvd_span_singleton, DirectSum.isInternal_biSup_submodule_of_iSupIndep, LinearMap.ker_le_range_iff, exists_mem_and_smul_eq_self_of_fg_of_le_smul, Ideal.map_toCotangent_ker, PrimeSpectrum.zeroLocus_empty_iff_eq_top, ProjectiveSpectrum.zeroLocus_inf, LinearMap.ofIsCompl_zero, LinearPMap.exists_of_le, Module.Baer.ExtensionOfMaxAdjoin.eqn, Pi.mem_span_range_single_inl_iff, span_biInter, sup_span, Ideal.smul_mem_pointwise_smul_iff, AffineSubspace.equivMapOfInjective_toFun, exteriorPower.ιMulti_family_span, ZSpan.fract_eq_fract, toLocalized'_apply_coe, mul_def, orthogonalProjection_comp_subtypeL_eq_zero_iff, PrimeSpectrum.zeroLocus_anti_mono_ideal, Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, dualQuotEquivDualAnnihilator_symm_apply_mk, LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate, Ideal.quotTorsionOfEquivSpanSingleton_apply_mk, Module.Basis.sumQuot_inl, ZLattice.sum_piFinset_Icc_rpow_le, LinearEquiv.ofInjective_symm_apply, Int.cast_mem_ideal_iff, LieAlgebra.Extension.twoCocycleOf_coe_coe, RingHom.surjectiveOnStalks_iff_forall_ideal, mem_map_equiv, closedComplemented_iff_isClosed_exists_isClosed_isCompl, EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem, ExteriorAlgebra.GradedAlgebra.ι_apply, Algebra.SubmersivePresentation.basisCotangent_apply, linearProjOfIsCompl_surjective, RootPairing.posRootForm_rootFormIn_posDef, Ideal.mem_span_pow_iff_exists_isHomogeneous, LinearMap.comp_ker_subtype, mulMap_range, AddMonoidAlgebra.single_mem_gradeBy, weightedVSub_mem_vectorSpan_pair, isFullyInvariant_iff_le_imp_isotypicComponent_le, TensorProduct.tensorQuotientEquiv_symm_apply_tmul_mk, groupHomology.coinvariantsKerOfIsBoundary₀_coe, Affine.Simplex.map_subtype_restrict, Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply, exteriorPower.oneEquiv_ιMulti, ConvexCone.mem_toPointedCone, Ideal.toIdeal_homogeneousHull_eq_iSup, Affine.Simplex.restrict_map_subtype, continuous_stereoInvFun, Algebra.Extension.Cotangent.map_mk, RootPairing.CoPolarizationIn_apply, Module.isTorsionBy_iff_mem_annihilator, mem_iSup_iff_exists_dfinsupp', orthogonalProjection_eq_zero_iff, linearDepOn_iff', groupCohomology.cocycles₁_ext_iff, CliffordAlgebra.GradedAlgebra.ι_sq_scalar, ZLattice.covolume.tendsto_card_div_pow'', Polynomial.sylveserMap_comp_adjSylvester, smul_mem_iff'', isAdic_iff, SkewMonoidAlgebra.mem_span_support, groupCohomology.map_H0Iso_hom_f_assoc, LinearMap.range_coe, AffineSubspace.subtypeₐᵢ_toAffineMap, exteriorPower.ιMulti_span, map_equivMapOfInjective_symm_apply, Finsupp.supportedEquivFinsupp_symm_apply_coe_apply, NonUnitalSubalgebra.coe_toSubmodule, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.num_mem_carrier_iff, orthogonalProjection_starProjection_of_le, Real.exists_extension_norm_eq, LinearMap.finrank_range_add_finrank_ker, IsCompl.projection_apply_mem, exteriorPower.toTensorPower_apply_ιMulti, coe_orthogonalProjection_apply, Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver, ModuleCat.kernelIsoKer_inv_kernel_ι, FractionalIdeal.mem_extended_iff, IsIsotypicOfType.isotypicComponent, Quotient.eq', coe_matrix, carrier_eq_coe, torsion'_torsion'_eq_top, instModuleFree_of_discrete_submodule, Representation.linHom.invariantsEquivRepHom_apply_hom, PeriodPair.ω₁_mem_lattice, starProjection_apply_eq_zero_iff, Ideal.natAbs_det_basis_change, ContinuousLinearMap.apply_val_ker, PadicInt.coe_dpow_eq, Module.Flat.iff_rTensor_injective', PeriodPair.analyticOnNhd_weierstrassP, AddMonoidAlgebra.grade.gradedMonoid, ModuleCat.imageIsoRange_hom_subtype_apply, skewAdjointPart_comp_subtype_skewAdjoint, Module.Basis.mem_span_repr_support, mem_top, mem_iSup_of_directed, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, HasStrictFDerivAt.implicitFunction_apply_image, SubmodulesRingBasis.mul, Polynomial.degreeLT.basisProd_castAdd, Polynomial.IsEisensteinAt.leading, MvPolynomial.coeffsIn_le, IsLocalization.map_algebraMap_ne_top_iff_disjoint, finrank_add_eq_of_isCompl, FG.generators_mem, Finsupp.supportedEquivFinsupp_apply_apply, FG.rTensor.directLimit_apply', finiteDimensional_of_le, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, IsLocalRing.local_hom_TFAE, Ideal.one_notMem, LieModule.Cohomology.d₂₃_comp_d₁₂, Subspace.quotDualCoannihilatorToDual_bijective, groupHomology.single_mem_cycles₁_iff, Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset, Affine.Simplex.affineSpan_pair_eq_altitude_iff, Ideal.toCotangent_surjective, lTensor_mkQ, norm_subtypeL_le, Finsupp.single_mem_supported, Ideal.coe_piOrderIso_apply, coe_scott_continuous, IsSemisimpleModule.range, ContinuousLinearEquiv.fst_equivOfRightInverse, coe_eq_univ, instFaithfulVAddSubtypeMem, exteriorPower.zeroEquiv_symm_apply, finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply, Module.AEval.mem_mapSubmodule_apply, Polynomial.IsWeaklyEisensteinAt.mem, Affine.Simplex.restrict_map_inclusion, basis_of_pid_aux, torsion'_isTorsion', DirectSum.isInternal_submodule_iff_isCompl, Polynomial.coeff_mem_contentIdeal, Ideal.mem_span_singleton_self, finiteDimensional_direction_affineSpan_singleton, EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq, sndEquiv_apply, instSMulCommClassSubtypeMemTorsion', RingHom.toKerIsLocalization_isLocalizedModule, sndEquiv_symm_apply_coe, Algebra.idealMap_apply_coe, comapSubtypeEquivOfLe_symm_apply, groupCohomology.map_id_comp_H0Iso_hom_assoc, PrimeSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal, groupCohomology.isoCocycles₂_hom_comp_i_assoc, Matrix.rank_eq_finrank_span_cols, EuclideanGeometry.orthogonalProjection_eq_iff_mem, IsLocalRing.isOpen_iff_finite_quotient, Nat.one_mem_span_iff, EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq, Absorbent.subset_range_iff_surjective, Module.Basis.mem_span_iff_repr_mem, Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_range, coe_subtypeL, mem_sSup, Rep.coindIso_hom_hom_hom, PrimeSpectrum.isCompact_isOpen_iff_ideal, HasStrictFDerivAt.implicitToPartialHomeomorph_apply_ker, orthogonalProjection_coe_eq_linearProjOfIsCompl, AffineMap.linear_eqOn_vectorSpan, IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_eq_one_iff, bot_colon, quotient_prod_linearEquiv, LinearMap.domRestrict₁₂_apply, PeriodPair.ω₂_mem_lattice, Ideal.map_includeLeft_eq, mem_graph_toLinearPMap, Algebra.Generators.H1Cotangent.equiv_apply, MeasureTheory.lpMeasToLpTrimLie_symm_toLp, groupCohomology.coe_mapCocycles₂, orthogonalProjection_norm_le, ContinuousLinearEquiv.equivOfRightInverse_symm_apply, span_le, LinearRecurrence.is_sol_iff_mem_solSpace, LinearMap.injective_rangeRestrict_iff, span_sInf, LinearDisjoint.rank_inf_le_one_of_flat_right, LinearMap.quotientInfEquivSupQuotient_surjective, colon_bot, LinearPMap.graph_map_snd_eq_range, PrimeSpectrum.zeroLocus_pow, ModuleCat.toKernelSubobject_arrow, orthogonalProjection_orthogonal, LinearMap.finrank_eigenspace_le, Module.Basis.SmithNormalForm.coord_apply_embedding_eq_smul_coord, LinearMap.domRestrict_apply, LinearMap.surjective_comp_subtype_of_isComplemented, affineSpan_insert_zero, Polynomial.taylorLinearEquiv_apply_coe, MeasureTheory.norm_condExpL2_le_one, mem_mk, LinearMap.mem_span_iff_continuous, Module.finrank_quotient_add_finrank_le, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_assoc, Module.Flat.iff_lTensor_injective', groupCohomology.H1π_eq_iff, Ideal.Fiber.exists_smul_eq_one_tmul, mem_span_insert, DirectSum.decompose_smul, Module.Basis.addSubgroupOfClosure_apply, AffineSubspace.vsub_left_mem_direction_iff_mem, MeasureTheory.condExpL2_comp_continuousLinearMap, Ideal.hasBasis_nhds_adic, mapsTo_span, Polynomial.mem_degreeLT, ZSpan.setFinite_inter, LinearEquiv.ofTop_apply, PeriodPair.derivWeierstrassPExcept_def, groupCohomology.isoCocycles₁_hom_comp_i_assoc, mulMap_comp_rTensor, coe_set_neg, Algebra.Extension.Cotangent.ker_mk, torsionBySet_isTorsionBySet, orthogonalProjection_orthogonalComplement_singleton_eq_zero, PointedCone.closure_eq, ClosedSubmodule.coe_toSubmodule, Polynomial.degreeLT.basis_repr, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end, ZLattice.coe_comap, Module.End.pos_finrank_genEigenspace_of_hasEigenvalue, LinearIsometry.submoduleMap_apply_coe, LinearDisjoint.rank_inf_le_one_of_flat_left, IsLocalization.coe_primeSpectrumOrderIso_apply_coe_asIdeal, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt, AddMonoidAlgebra.mem_gradeBy_iff, Polynomial.IsEisensteinAt.notMem, orthogonalProjection_eq_linearProjOfIsCompl, groupHomology.mapCycles₁_quotientGroupMk'_epi, Quotient.mk_eq_zero, inf_coe, RootPairing.range_polarizationIn_le_span_coroot, HomogeneousIdeal.mem_iff, groupHomology.mapCycles₁_comp_i_assoc, exists_smith_normal_form_of_le, PowerSeries.IsWeierstrassDivisorAt.coeff_div_sub_seq_mem, linearDepOn_iff'ₛ, MeasureTheory.condExpL2_const_inner, LinearPMap.toFun_eq_coe, exteriorPower.ιMulti_family_apply_coe, PrimeSpectrum.le_vanishingIdeal_zeroLocus, map_subtype_le, IsCoercive.isClosed_range, mem_traceDual_iff_isIntegral, AffineEquiv.ofEq_rfl, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_apply, IsLocalization.mem_span_iff, PadicInt.existsUnique_mem_range, LinearMap.finiteDimensional_range, coe_prodEquivOfClosedCompl, Module.Basis.restrictScalars_toMatrix, Nat.coe_maximalIdeal, IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff, TensorProduct.exists_of_fg, torsionBy.mk_smul, AddMonoidAlgebra.mem_span_support, Subalgebra.rank_toSubmodule, groupHomology.π_comp_H2Iso_inv_apply, mem_torsion'_iff, Valuation.Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow, Polynomial.IsEisensteinAt.coeff_mem, LinearMap.BilinForm.restrict_apply, groupCohomology.coboundariesOfIsCoboundary₂_coe, topologicalClosure.completeSpace, DirectSum.range_coeLinearMap, PadicInt.toZMod_spec, submoduleOf_self, LinearPMap.mem_range_iff, EuclideanGeometry.dist_set_eq_iff_dist_orthogonalProjection_eq, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_source, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure, HasStrictFDerivAt.eq_implicitFunction, Finsupp.range_restrictDom, starProjection_eq_self_iff, Projectivization.Subspace.mem_submodule_iff, Ideal.mem_inv_pointwise_smul_iff, LinearMap.BilinForm.nondegenerate_restrict_of_disjoint_orthogonal, linearIndepOn_iff_linearCombinationOnₛ, finiteDimensional_inf_left, EuclideanGeometry.Sphere.finrank_orthRadius, ContinuousLinearEquiv.ofSubmodule'_toContinuousLinearMap, TwoSidedIdeal.coe_asIdeal, LinearMap.rank_range_add_rank_ker, finrank_vectorSpan_insert_le_set, coe_equivMapOfInjective_apply, mem_neg, mem_iSup, Ideal.IsPrime.mul_mem_iff_mem_or_mem, MvPolynomial.mem_ideal_span_X_image, LinearMap.exists_map_addHaar_eq_smul_addHaar', InnerProductSpace.gramSchmidt_mem_span, MvPolynomial.mem_restrictTotalDegree, iSupIndep_iff_forall_dfinsupp, IsLinearTopology.hasBasis_right_ideal, disjoint_iff_comap_eq_bot, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem, groupHomology.mem_cycles₁_iff, instProperSpaceSubtypeMemSubmoduleOfCompleteSpaceOfLocallyCompactSpace, LinearMap.lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm, LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces, Subspace.finrank_add_finrank_dualAnnihilator_eq, IsDedekindDomain.isOpen_iff, TensorProduct.toLinearMap_mapInclIsometry, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, small_sup, FiniteArchimedeanClass.mem_closedBall_iff, existsUnique_add_of_isCompl_prod, SimpleGraph.mem_ker_toLin'_lapMatrix_of_connectedComponent, MvPolynomial.coe_coeffsIn, RootPairing.algebraMap_root'In_apply, groupCohomology.mapCocycles₁_comp_i, groupHomology.boundariesToCycles₁_apply, orthonormal_span, groupHomology.single_mem_cycles₂_iff_inv, MvPolynomial.mem_image_comap_C_basicOpen, TensorProduct.range_mapIncl_mono, surjective_stereographic, Module.Finite.of_isComplemented_codomain, MatrixModCat.fromMatrixLinear_apply_coe, mem_closure_iff, coe_ofLinearComb, coe_toAddSubgroup, PeriodPair.finrank_lattice, PeriodPair.derivWeierstrassP_add_coe, IsLocalRing.isOpen_maximalIdeal, Algebra.Presentation.mem_ker_naive, linearIndepOn_iff_linearCombinationOn, PointedCone.dual_eq_iInter_dual_singleton, Module.Flat.instInvertibleSubtypeMemSubmoduleSubmoduleAlgebra, LinearMap.toKerIsLocalized_apply_coe, coe_sInf, LinearMap.submoduleMap_surjective, hasFDerivAt_stereoInvFunAux_comp_coe, LinearIsometryEquiv.ofEq_symm, AffineSubspace.isClosed_direction_iff, finiteDimensional_vectorSpan_insert, LinearPMap.inverse_domain, exteriorPower.basis_repr_self, PointedCone.dual_dual_flip_dual, Ideal.mem_prod, MeasureTheory.condExpL2_indicator_nonneg, flip_quotDualCoannihilatorToDual_injective, PointedCone.coe_comap, coe_prodEquivOfClosedCompl_symm, isClosed_or_dense_of_isCoatom, groupCohomology.cocycles₁.d₁₂_apply, Module.Finite.instLinearMapIdSubtypeMemSubmoduleOfIsSemisimpleModule, Algebra.Extension.cotangentComplex_mk, mulRightMap_apply_single, MvPolynomial.WeightedHomogeneousSubmodule.gradedMonoid, RingHom.surjective_localRingHom_iff, Subspace.dualPairing_eq, groupHomology.isoCycles₂_hom_comp_i_assoc, IdealFilter.isUniform_iff_exists_ringFilterBasis, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, subalgebra_top_rank_eq_submodule_top_rank, Int.submodule_toAddSubgroup_index_ne_zero_iff, fstEquiv_apply, groupCohomology.π_comp_H2Iso_hom, FiniteDimensional.span_singleton, Ideal.to_quotient_square_comp_toCotangent, retractionOfSectionOfKerSqZero_tmul_D, Ideal.IsHomogeneous.mem_iff, groupHomology.H2π_eq_zero_iff, finrank_vectorSpan_range_le, ContinuousLinearEquiv.ofSubmodules_apply, AffineSubspace.coe_direction_eq_vsub_set_right, Ideal.mem_jacobson_bot, LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul, BoxIntegral.unitPartition.tag_mem_smul_span, LinearMap.ofIsCompl_eq_add, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus, span_range_inclusionSpan, PeriodPair.weierstrassPExcept_add, LinearMap.surjective_domRestrict_iff, coe_iSup_of_chain, span_coe_eq_restrictScalars, surjOn_iff_le_map, ZLattice.exists_finsetSum_norm_rpow_le_tsum, mem_nilradical, Subspace.dualEquivDual_apply, isHilbertSumOrthogonal, instIsLocalizedModuleSubtypeMemLocalized₀ToLocalized₀, Affine.Simplex.restrict_points_coe, Ideal.isoBaseOfIsPrincipal_apply, smul_coe, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, ZLattice.abs_repr_le, Affine.Simplex.excenterExists_restrict, MvPolynomial.decomposition.decompose'_eq, restrictScalarsEquiv_apply, ZLattice.covolume_eq_det, Algebra.Generators.C_mul_X_sub_one_mem_ker, RingFilterBasis.SubmodulesBasis.smul, Finsupp.mem_supported', rank_range_of_surjective, PointedCone.salient_iff_inter_neg_eq_singleton, card_eq_card_quotient_mul_card, Ideal.isOpen_of_isMaximal, Ideal.span_singleton_mul_le_iff, Valuation.HasExtension.algebraMap_mem_maximalIdeal_iff, EuclideanGeometry.orthogonalProjection_mem_subspace_eq_self, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_apply, natAbs_det_basis_change, exists_sub_one_mem_and_smul_le_of_fg_of_le_sup, NumberField.mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply, orthogonalProjectionFn_mem, groupHomology.H1π_eq_iff, nonempty_basis_of_pid, LinearIsometryEquiv.submoduleMap_apply_coe, PointedCone.dual_span, comap_subtype_le_iff, MeasureTheory.lpMeas.aestronglyMeasurable, mem_iff_norm_starProjection, isSemisimpleModule_iff_exists_linearEquiv_dfinsupp, groupHomology.cyclesMap_comp_isoCycles₁_hom, PeriodPair.differentiableOn_derivWeierstrassPExcept, PrimeSpectrum.zeroLocus_eq_singleton, ContinuousLinearEquiv.ofSubmodules_symm_apply, KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span, Module.notMem_support_iff', Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective, PowerSeries.IsWeierstrassDivisionAt.coeff_f_sub_r_mem, exists_linearIndepOn_id_extension, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff, HahnEmbedding.Partial.toOrderAddMonoidHom_injective
smul 📖	CompOp	35 math math: instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe, OrthonormalBasis.orthogonalProjection_eq_sum, isScalarTower, LinearMap.IsSymmetric.diagonalization_apply_self_apply, OrthonormalBasis.orthogonalProjection_apply_eq_sum, Module.Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul, isSMulRegular_submodule_iff_right_eq_zero_of_smul, HilbertBasis.hasSum_orthogonalProjection, stereoToFun_apply, IsSMulRegular.submodule, lTensorOne'_tmul, rTensorOne'_tmul, isScalarTower', rTensorOne_tmul, instIsScalarTowerQuotientSpanSingletonSetSubtypeMemTorsionBy, torsionBy.mk_ideal_smul, LinearPMap.map_smul, LieModule.Cohomology.smul_apply_apply, isCentralScalar, coe_smul, restrictScalars.isScalarTower, coe_smul_of_tower, smul_torsionBy, stereographic_apply, lTensorOne_tmul, isScalarTower_of_section_of_ker_sqZero, torsionBySet.mk_smul, UniformOnFun.continuousSMul_submodule_of_image_bounded, isSMulRegular_on_submodule_iff_disjoint_ker_lsmul_submodule, MeasureTheory.lpMeasToLpTrim_smul, mem_set_smul, Ideal.quotTorsionOfEquivSpanSingleton_apply_mk, exteriorPower.zeroEquiv_symm_apply, instSMulCommClassSubtypeMemTorsion', torsionBy.mk_smul
toAddSubgroup 📖	CompOp	60 math math: toAddSubgroup_toZModSubmodule, LinearMap.range_toAddSubgroup, FiniteArchimedeanClass.toAddSubgroup_ball, ContinuousMap.range_toLp, SubmodulesRingBasis.toRing_subgroups_basis, ZLattice.comap_toAddSubgroup, pointwise_smul_toAddSubgroup, AdjoinRoot.evalEval_apply, torsion_int, NumberField.Units.span_basisOfIsMaxRank, Quotient.quotientAddGroupMk_eq_mk, AddSubgroup.toZModSubmodule_toAddSubgroup, exists_finiteIndex_of_cover, span_int_eq, ZLattice.covolume_div_covolume_eq_relIndex, toAddSubgroup_toAddSubmonoid, Ideal.index_pow_le, AddSubgroup.toIntSubmodule_symm, top_toAddSubgroup, Ideal.Quotient.index_eq_zero, RingPreordering.supportAddSubgroup_eq, toAddSubgroup_mono, span_singleton_toAddSubgroup_eq_zmultiples, toIntSubmodule_toAddSubgroup, toAddSubgroup_injective, toAddSubgroup_toIntSubmodule, span_int_eq_addSubgroup_closure, ZSpan.isAddFundamentalDomain', fg_iff_addSubgroup_fg, AddSubgroup.toZModSubmodule_symm, mem_toAddSubgroup, lp.coe_lpSubmodule, span_int_eq_addSubgroupClosure, goursatSnd_toAddSubgroup, toAddSubgroup_strictMono, Ideal.span_singleton_toAddSubgroup_eq_zmultiples, ArchimedeanClass.toAddSubgroup_ball, goursatFst_toAddSubgroup, ZSpan.instDiscreteTopologySubtypeMemAddSubgroupToAddSubgroupIntSpanRangeCoeBasisRealOfFinite, Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_pow_mul_prod, toAddSubgroup_eq_top, fg_iff_add_subgroup_fg, Ideal.pointwise_smul_toAddSubgroup, MeasureTheory.Lp.coe_LpSubmodule, AddSubgroup.toIntSubmodule_toAddSubgroup, map_toAddSubgroup, index_smul_le, FiniteArchimedeanClass.toAddSubgroup_closedBall, toAddSubgroup_le, Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_ite, BoundedContinuousFunction.range_toLp, LinearMap.ker_toAddSubgroup, KaehlerDifferential.quotKerTotalEquiv_apply, toAddSubgroup_inj, sup_toAddSubgroup, bot_toAddSubgroup, ZLattice.covolume_div_covolume_eq_relIndex', coe_toAddSubgroup, ArchimedeanClass.toAddSubgroup_closedBall, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply
toAddSubmonoid 📖	CompOp	61 math math: toAddSubmonoid_toNatSubmodule, Ideal.Filtration.submodule_closure_single, span_nat_eq_addSubmonoid_closure, top_toAddSubmonoid, coe_toAddSubmonoid, toAddSubmonoid_injective, toSubalgebra_toSubsemiring, ClosedSubmodule.coe_sSup, coe_toSubalgebra, closure_le_toAddSubmonoid_span, LinearMap.range_toAddSubmonoid, HomogeneousIdeal.toAddSubmonoid_irrelevant_le, span_nat_eq, LieSubalgebra.mem_carrier, AddSubmonoid.toNatSubmodule_toAddSubmonoid, le_one_toAddSubmonoid, Ideal.disjoint_powers_iff_notMem, toAddSubgroup_toAddSubmonoid, toAddSubmonoid_strictMono, pointwise_smul_toAddSubmonoid, ClosedSubmodule.ext_iff, LinearMap.ker_toAddSubmonoid, bot_toAddSubmonoid, HomogeneousIdeal.irrelevant_le, toAddSubmonoid_mono, smul_toAddSubmonoid, toAddSubmonoid_sSup, span_eq_closure, AddSubmonoid.toNatSubmodule_symm, mul_toAddSubmonoid, ClosedSubmodule.mem_sup, ClosedSubmodule.mem_iSup, fg_iff_addSubmonoid_fg, toAddSubmonoid_le, mem_toAddSubmonoid, Representation.invariants_eq_inter, Subalgebra.pi_toSubsemiring, span_nat_eq_addSubmonoidClosure, toAddSubmonoid_inj, ClosedSubmodule.mem_sSup, mem_carrier, Subalgebra.coe_pi, LinearMap.eqLocus_toAddSubmonoid, toAddSubmonoid_restrictScalars, HomogeneousIdeal.irrelevant_eq_iSup, LieSubmodule.mem_carrier, sup_toAddSubmonoid, HomogeneousIdeal.irrelevant_eq_closure, ClosedSubmodule.coe_iSup, HomogeneousIdeal.toIdeal_irrelevant_le, map_toAddSubmonoid', ClosedSubmodule.coe_sup, neg_toAddSubmonoid, carrier_eq_coe, pow_toAddSubmonoid, iSup_toAddSubmonoid, le_pow_toAddSubmonoid, ClosedSubmodule.carrier_eq_coe, map_toAddSubmonoid, Ideal.pointwise_smul_toAddSubmonoid, ClosedSubmodule.isClosed'
toSubMulAction 📖	CompOp	6 math math: toSubMulAction_inj, toSubMulAction_strictMono, coe_toSubMulAction, toSubMulAction_one, toSubMulAction_injective, toSubMulAction_mono
zero 📖	CompOp	73 math math: HasStrictFDerivAt.map_implicitFunctionOfComplemented_eq, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, iSupIndep.linearEquiv_symm_apply, linearProjOfIsCompl_apply_right, prodEquivOfIsCompl_symm_apply_snd_eq_zero, Ideal.finsuppTotal_apply_eq_of_fintype, eq_zero_of_coe_mem_of_disjoint, Ideal.finsuppTotal_apply, linearProjOfIsCompl_apply_right', HasStrictFDerivAt.mem_implicitToPartialHomeomorphOfComplemented_target, Polynomial.degreeLT.addLinearEquiv_castAdd, IsCompactOperator.restrict', mulLeftMap_apply, stereographic_apply_neg, HasStrictFDerivAt.to_implicitFunctionOfComplemented, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_target, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, mem_left_iff_eq_zero_of_disjoint, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, botEquivPUnit_symm_apply, LinearDisjoint.linearIndependent_right_of_flat, HasStrictFDerivAt.map_implicitFunction_eq, HasStrictFDerivAt.implicitToPartialHomeomorph_self, prodEquivOfIsCompl_symm_apply_fst_eq_zero, DirectSum.IsInternal.ofBijective_coeLinearMap_of_mem_ne, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_target, HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented_self, LinearPMap.map_zero, HasStrictFDerivAt.to_implicitFunction, Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, coe_zero, HasStrictFDerivAt.implicitToPartialHomeomorphOfComplemented_self, IsCompactOperator.restrict, prodEquivOfIsCompl_symm_apply_left, stereographic_neg_apply, iSupIndep.linearEquiv_apply, Function.Exact.linearMap_rangeRestrict, ZSpan.isAddFundamentalDomain, mem_right_iff_eq_zero_of_disjoint, mulRightMap_apply, Function.Exact.iff_linearMap_rangeRestrict, HasStrictFDerivAt.implicitToOpenPartialHomeomorph_self, ContinuousLinearMap.projKerOfRightInverse_comp_inv, prodEquivOfIsCompl_symm_apply_right, mulLeftMap_apply_single, Ideal.range_finsuppTotal, ZLattice.isAddFundamentalDomain, coe_eq_zero, smul_torsionBy, CliffordAlgebra.even.lift.aux_apply, ClosedComplemented.exists_submodule_equiv_prod, Polynomial.degreeLT.addLinearEquiv_natAdd, orthogonalProjection_orthogonal_apply_eq_zero, DirectSum.IsInternal.ofBijective_coeLinearMap_of_ne, eq_zero_of_bot_submodule, IsIsotypic.linearEquiv_finsupp, HasStrictFDerivAt.mem_implicitToPartialHomeomorph_target, EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection, Polynomial.degreeLT.basisProd_natAdd, mem_set_smul, linearProjOfIsCompl_apply_eq_zero_iff, HasStrictFDerivAt.implicitFunctionOfComplemented_apply_image, mem_iSup_iff_exists_dfinsupp', LinearDisjoint.linearIndependent_left_of_flat, orthogonalProjection_eq_zero_iff, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, HasStrictFDerivAt.implicitFunction_apply_image, Polynomial.degreeLT.basisProd_castAdd, mk_eq_zero, orthogonalProjection_orthogonalComplement_singleton_eq_zero, iSupIndep_iff_forall_dfinsupp, hasFDerivAt_stereoInvFunAux_comp_coe, mulRightMap_apply_single

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addSubgroupClass 📖	mathematical	—	AddSubgroupClass Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup setLike	—	addSubmonoidClass SubMulAction.neg_mem
addSubmonoidClass 📖	mathematical	—	AddSubmonoidClass Submodule AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid setLike	—	AddSubsemigroup.add_mem' AddSubmonoid.zero_mem'
add_mem 📖	mathematical	Submodule SetLike.instMembership setLike	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	AddMemClass.add_mem AddSubmonoidClass.toAddMemClass addSubmonoidClass
add_mem_iff_left 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	add_mem_cancel_right addSubgroupClass
add_mem_iff_right 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	add_mem_cancel_left addSubgroupClass
carrier_eq_coe 📖	mathematical	—	AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.toAddSubsemigroup toAddSubmonoid SetLike.coe Submodule setLike	—	—
coe_add 📖	mathematical	—	Submodule SetLike.instMembership setLike add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
coe_copy 📖	mathematical	SetLike.coe Submodule setLike	copy	—	—
coe_eq_zero 📖	mathematical	—	Submodule SetLike.instMembership setLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid zero	—	SetLike.coe_eq_coe
coe_mem 📖	mathematical	—	Submodule SetLike.instMembership setLike	—	—
coe_mk 📖	—	Submodule SetLike.instMembership setLike	—	—	—
coe_neg 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike NegMemClass.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddSubgroupClass.toNegMemClass AddGroup.toSubNegMonoid AddCommGroup.toAddGroup addSubgroupClass	—	NegMemClass.coe_neg addSubgroupClass
coe_ofClass 📖	mathematical	—	SetLike.coe Submodule setLike ofClass	—	—
coe_ofLinearComb 📖	mathematical	Set.Nonempty Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	SetLike.coe Submodule setLike ofLinearComb	—	—
coe_set_mk 📖	mathematical	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.toAddSubsemigroup SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	SetLike.coe Submodule setLike AddSubmonoid AddSubmonoid.instSetLike	—	—
coe_smul 📖	mathematical	—	Submodule SetLike.instMembership setLike smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass instDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommMonoid.toAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction	—	IsScalarTower.left
coe_smul_of_tower 📖	mathematical	—	Submodule SetLike.instMembership setLike smul	—	—
coe_sub 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike AddSubgroupClass.sub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup addSubgroupClass SubNegMonoid.toSub	—	AddSubgroupClass.coe_sub addSubgroupClass
coe_toAddSubgroup 📖	mathematical	—	SetLike.coe AddSubgroup AddCommGroup.toAddGroup AddSubgroup.instSetLike toAddSubgroup Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid setLike	—	—
coe_toAddSubmonoid 📖	mathematical	—	SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.instSetLike toAddSubmonoid Submodule setLike	—	—
coe_toSubMulAction 📖	mathematical	—	SetLike.coe SubMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SubMulAction.instSetLike toSubMulAction Submodule setLike	—	—
coe_zero 📖	mathematical	—	Submodule SetLike.instMembership setLike zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
copy_eq 📖	mathematical	SetLike.coe Submodule setLike	copy	—	SetLike.coe_injective
eta 📖	—	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.toAddSubsemigroup toAddSubmonoid SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—	—
ext 📖	—	Submodule SetLike.instMembership setLike	—	—	SetLike.ext
ext_iff 📖	mathematical	—	Submodule SetLike.instMembership setLike	—	ext
instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallHSMul 📖	mathematical	—	CanLift Set Submodule SetLike.coe setLike Set.instMembership AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
isScalarTower 📖	mathematical	—	IsScalarTower Submodule SetLike.instMembership setLike smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass instDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommMonoid.toAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction	—	SubMulAction.isScalarTower
isScalarTower' 📖	mathematical	—	IsScalarTower Submodule SetLike.instMembership setLike smul	—	SubMulAction.isScalarTower'
mem_carrier 📖	mathematical	—	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.toAddSubsemigroup toAddSubmonoid SetLike.coe Submodule setLike	—	—
mem_mk 📖	mathematical	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.toAddSubsemigroup SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Submodule SetLike.instMembership setLike AddSubmonoid AddSubmonoid.instSetLike	—	—
mem_toAddSubgroup 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike toAddSubgroup Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid setLike	—	—
mem_toAddSubmonoid 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubmonoid.instSetLike toAddSubmonoid Submodule setLike	—	—
mk_eq_zero 📖	mathematical	Submodule SetLike.instMembership setLike	zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
mk_le_mk 📖	mathematical	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.toAddSubsemigroup SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder AddSubmonoid AddSubmonoid.instPartialOrder	—	—
neg_mem 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	NegMemClass.neg_mem AddSubgroupClass.toNegMemClass addSubgroupClass
neg_mem_iff 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	neg_mem_iff AddSubgroupClass.toNegMemClass addSubgroupClass
nonempty 📖	mathematical	—	Set.Nonempty SetLike.coe Submodule setLike	—	zero_mem
smulMemClass 📖	mathematical	—	SMulMemClass Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction setLike	—	SubMulAction.smul_mem'
smul_mem 📖	mathematical	Submodule SetLike.instMembership setLike	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	smul_mem'
smul_mem' 📖	mathematical	Set Set.instMembership AddSubsemigroup.carrier AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.toAddSubsemigroup toAddSubmonoid	SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
smul_mem_iff' 📖	mathematical	—	Submodule SetLike.instMembership setLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction	—	SubMulAction.smul_mem_iff'
smul_mem_iff'' 📖	mathematical	—	Submodule SetLike.instMembership setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	invOf_smul_smul smul_mem
smul_mem_iff_of_isUnit 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Submodule SetLike.instMembership setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction	—	smul_mem_iff''
smul_of_tower_mem 📖	—	Submodule SetLike.instMembership setLike	—	—	SubMulAction.smul_of_tower_mem
sub_mem 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_mem addSubgroupClass
sub_mem_iff_left 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_eq_add_neg add_mem_iff_left neg_mem
sub_mem_iff_right 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_eq_add_neg add_mem_iff_right neg_mem_iff
toAddSubgroup_inj 📖	mathematical	—	toAddSubgroup	—	toAddSubgroup_injective
toAddSubgroup_injective 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid AddSubgroup AddCommGroup.toAddGroup toAddSubgroup	—	SetLike.ext SetLike.ext_iff
toAddSubmonoid_inj 📖	mathematical	—	toAddSubmonoid	—	toAddSubmonoid_injective
toAddSubmonoid_injective 📖	mathematical	—	Submodule AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid toAddSubmonoid	—	SetLike.ext'_iff
toSubMulAction_inj 📖	mathematical	—	toSubMulAction	—	toSubMulAction_injective
toSubMulAction_injective 📖	mathematical	—	Submodule SubMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction toSubMulAction	—	SetLike.ext'_iff
zero_mem 📖	mathematical	—	Submodule SetLike.instMembership setLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass addSubmonoidClass

SubmoduleClass

Definitions

Name	Category	Theorems
module' 📖	CompOp	—

---

← Back to Index