Basic

📁 Source: Mathlib/Algebra/Group/Pi/Basic.lean

Statistics

Metric	Count
Definitions addCancelCommMonoid, addCancelMonoid, addCommGroup, addCommMonoid, addCommSemigroup, addGroup, addLeftCancelMonoid, addLeftCancelSemigroup, addMonoid, addRightCancelMonoid, addRightCancelSemigroup, addSemigroup, addZeroClass, cancelCommMonoid, cancelMonoid, commGroup, commMonoid, commSemigroup, divInvMonoid, divInvOneMonoid, divisionCommMonoid, divisionMonoid, group, instSubtractionCommMonoid, invOneClass, involutiveInv, involutiveNeg, leftCancelMonoid, leftCancelSemigroup, monoid, mulOneClass, negZeroClass, rightCancelMonoid, rightCancelSemigroup, semigroup, subNegMonoid, subNegZeroMonoid, subtractionMonoid, uniqueOfSurjectiveOne, uniqueOfSurjectiveZero	40
Theorems comp_eq_const_iff, comp_eq_one_iff, comp_eq_zero_iff, comp_ne_one_iff, comp_ne_zero_iff, extend_add, extend_div, extend_inv, extend_mul, extend_neg, extend_one, extend_sub, extend_zero, instIsCancelAdd, instIsCancelMul, instIsLeftCancelAdd, instIsLeftCancelMul, instIsRightCancelAdd, instIsRightCancelMul, pi_mulSingle_eq, pi_single_eq, elim_add_add, elim_div_div, elim_inv_inv, elim_mulSingle_one, elim_mul_mul, elim_neg_neg, elim_one_mulSingle, elim_one_one, elim_single_zero, elim_sub_sub, elim_zero_single, elim_zero_zero	33
Total	73

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_eq_const_iff 📖	—	—	—	—	Injective.comp_left
comp_eq_one_iff 📖	mathematical	—	Pi.instOne	—	comp_eq_const_iff
comp_eq_zero_iff 📖	mathematical	—	Pi.instZero	—	comp_eq_const_iff
comp_ne_one_iff 📖	—	—	—	—	Iff.ne comp_eq_one_iff
comp_ne_zero_iff 📖	—	—	—	—	Iff.ne comp_eq_zero_iff
extend_add 📖	mathematical	—	extend Pi.instAdd	—	extend_def apply_dite₂
extend_div 📖	mathematical	—	extend Pi.instDiv	—	extend_def apply_dite₂
extend_inv 📖	mathematical	—	extend Pi.instInv	—	extend_def
extend_mul 📖	mathematical	—	extend Pi.instMul	—	extend_def apply_dite₂
extend_neg 📖	mathematical	—	extend Pi.instNeg	—	extend_def
extend_one 📖	mathematical	—	extend Pi.instOne	—	—
extend_sub 📖	mathematical	—	extend Pi.instSub	—	extend_def apply_dite₂
extend_zero 📖	mathematical	—	extend Pi.instZero	—	—

Pi

Definitions

Name	Category	Theorems
addCancelCommMonoid 📖	CompOp	—
addCancelMonoid 📖	CompOp	—
addCommGroup 📖	CompOp	630 math math: Matrix.l2_opNorm_toEuclideanCLM, OrthonormalBasis.singleton_repr, comul_eq_adjoint, Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_left_iff, hasFDerivWithinAt_pi'', DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply, Rep.resCoindHomEquiv_apply_hom, groupCohomology.instEpiModuleCatH2π, PiLp.continuousLinearEquiv_symm_apply, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, Affine.Simplex.affineCombination_mem_closedInterior_iff, hasStrictFDerivAt_apply, differentiableWithinAt_finCons', Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_left_iff, PiLp.basisFun_equivFun, Finset.affineCombination_vsub, ModuleCat.biproductIsoPi_inv_comp_π, groupCohomology.toCocycles_comp_isoCocycles₁_hom, groupCohomology.isoCocycles₁_hom_comp_i_apply, Finset.affineCombination_affineCombinationSingleWeights, AddCommGrpCat.biproductIsoPi_inv_comp_π_apply, instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere, tendsto_tsum_div_pow_atTop_integral, NumberField.canonicalEmbedding.mem_span_latticeBasis, hasStrictFDerivAt_list_prod_finRange', groupCohomology.d₂₃_hom_apply, NumberField.Units.logEmbedding_fundSystem, LinearIsometryEquiv.piLpCongrRight_symm, ContinuousMultilinearMap.norm_iteratedFDerivComponent_le, Finset.affineCombination_apply_eq_lineMap_sum, hasFDerivAtFilter_pi, Finset.centroid_eq_affineCombination_fintype, EuclideanSpace.closedBall_zero_eq, hasFDerivAt_multiset_prod, OrthonormalBasis.repr_injective, groupCohomology.d₀₁_comp_d₁₂, Matrix.spectrum_toEuclideanLin, Matrix.iSup_eigenspace_toLin'_diagonal_eq_top, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, ModuleCat.toMatrixModCat_map, Matrix.cstar_nnnorm_def, groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply, Rep.resCoindAdjunction_counit_app_hom_hom, AffineMap.pi_lineMap_apply, Matrix.l2_opNorm_mulVec, groupCohomology.eq_d₀₁_comp_inv, groupCohomology.H1π_comp_map_assoc, differentiableWithinAt_pi'', groupCohomology.π_comp_H1Iso_hom_assoc, LinearMap.IsSymmetric.diagonalization_apply_self_apply, Finset.affineCombination_sdiff_sub, groupCohomology.eq_d₁₂_comp_inv, groupCohomology.mapCocycles₂_comp_i, LinearMap.det_pi, NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, Matrix.spectrum_toLpLin, NumberField.mixedEmbedding.mem_idealLattice, BoxIntegral.unitPartition.mem_smul_span_iff, differentiableOn_pi, groupCohomology.coe_mapCocycles₁, AffineMap.proj_linear, LieModule.instIsFaithfulMatrixForall, groupCohomology.d₁₂_hom_apply, Behrend.sphere_subset_preimage_metric_sphere, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_assoc, Submodule.quotientPi_aux.map_smul, Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.wOppSide_affineSpan_faceOpposite_point_right_iff, ProbabilityTheory.HasGaussianLaw.toLp_pi, Affine.Simplex.ExcenterExists.affineCombination_eq_excenter_iff, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂, groupCohomology.comp_d₁₂_eq, ModuleCat.toMatrixModCat_obj_isAddCommGroup, groupCohomology.cocycles₂.d₂₃_apply, groupCohomology.d₀₁_hom_apply, OrthonormalBasis.repr_self, hasDerivWithinAt_pi, LinearMap.spectrum_toMatrix', LinearIsometryEquiv.piLpCongrRight_apply, AffineIndependent.affineCombination_eq_iff_eq, groupCohomology.dArrowIso₀₁_inv_right, groupCohomology.d₁₂_comp_d₂₃_apply, Matrix.toLpLin_mul_same, groupCohomology.eq_d₂₃_comp_inv_assoc, groupCohomology.eq_d₂₃_comp_inv_apply, OrthonormalBasis.measurePreserving_repr, groupCohomology.eq_d₁₂_comp_inv_apply, differentiable_finCons', RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, CStarMatrix.toCLM_injective, Finset.affineCombination_apply_const, hasStrictFDerivAt_pi', PiLp.coe_continuousLinearEquiv, LinearMap.rank_diagonal, Matrix.toEuclideanLin_apply, Rep.resCoindAdjunction_unit_app_hom_hom, hasFDerivWithinAt_pi', fderivWithin_pi, Euclidean.closedBall_eq_image, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, groupCohomology.mapCocycles₂_comp_i_apply, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_apply, MeasureTheory.charFunDual_pi', differentiable_apply, CStarMatrix.norm_def', BoxIntegral.unitPartition.integralSum_eq_tsum_div, Quaternion.linearIsometryEquivTuple_symm_apply, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, counit_eq_adjoint, AdicCompletion.pi_apply_coe, ModuleCat.HasLimit.productLimitCone_cone_π, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply, CStarMatrix.inner_toCLM_conjTranspose_left, tendsto_card_div_pow_atTop_volume, EuclideanSpace.instFactEqNatFinrankFin, differentiable_euclidean, Affine.Simplex.excenter_eq_affineCombination, groupCohomology.mapCocycles₂_comp_i_assoc, groupCohomology.H1IsoOfIsTrivial_inv_apply, EuclideanSpace.volume_closedBall_fin_three, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, hasStrictFDerivAt_multiset_prod, groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, groupCohomology.H2π_comp_map_apply, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, affineCombination_mem_affineSpan_pair, groupCohomology.dArrowIso₀₁_hom_right, QuadraticMap.Ring.polarBilin_pi, ContinuousLinearMap.det_pi, PiLp.sumPiLpEquivProdLpPiLp_symm_apply_ofLp, groupCohomology.toCocycles_comp_isoCocycles₂_hom, Module.Basis.coe_toOrthonormalBasis_repr, iteratedFDeriv_sum, Affine.Simplex.affineCombination_mem_interior_face_iff_mem_Ioo, hasFDerivAt_finCons, ZLattice.covolume.tendsto_card_div_pow, hasFDerivWithinAt_finCons, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_assoc, Finset.affineCombination_congr, Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenter, Finset.affineCombination_eq_linear_combination, NumberField.Units.span_basisOfIsMaxRank, PiLp.volume_preserving_toLp, Module.rankAtStalk_pi, Finset.sum_smul_const_vsub_eq_vsub_affineCombination, Affine.Simplex.affineCombination_mem_closedInterior_face_iff_nonneg, groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply, LinearIsometryEquiv.piLpCongrLeft_apply, AffineMap.pi_apply, groupCohomology.comp_d₂₃_eq, mem_affineSpan_iff_eq_affineCombination, OrthonormalBasis.coe_ofRepr, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, PiLp.sub_apply, Complex.orthonormalBasisOneI_repr_apply, groupCohomology.d₁₂_apply_mem_cocycles₂, Matrix.toLpLin_symm_pow, differentiableOn_finCons', groupCohomology.d₀₁_apply_mem_cocycles₁, Finset.affineCombination_of_eq_one_of_eq_zero, affineCombination_mem_affineSpan, dist_affineCombination_lt_of_strictConvexSpace, coe_addEquiv_lpPiLp_symm, differentiableAt_apply, Matrix.toEuclideanCLM_toLp, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, groupCohomology.subtype_comp_d₀₁_apply, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, differentiableAt_pi'', AddCommGrpCat.HasLimit.productLimitCone_isLimit_lift, Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenter, groupCohomology.H2π_eq_iff, groupCohomology.comp_d₀₁_eq, Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_left_iff, PiLp.hasFDerivAt_toLp, Projectivization.cross_mk_of_cross_ne_zero, Matrix.toLpLin_one, deriv_pi, EuclideanSpace.volume_closedBall_fin_two, Finset.attach_affineCombination_coe, hasFDerivAt_apply, Matrix.piLp_ofLp_toEuclideanLin, eq_affineCombination_of_mem_affineSpan_image, LinearMap.IsSymmetric.diagonalization_symm_apply, lieEquivMatrix'_apply, AffineMap.proj_apply, Finset.map_affineCombination, OrthonormalBasis.tensorProduct_repr_tmul_apply', groupCohomology.dArrowIso₀₁_inv_left, groupCohomology.π_comp_H1Iso_hom, LinearMap.minpoly_toMatrix', Matrix.l2_opNNNorm_mulVec, NumberField.mixedEmbedding.span_idealLatticeBasis, Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff, hasFDerivWithinAt_finCons', PiLp.basisFun_repr, Matrix.toLpLin_pow, RootPairing.GeckConstruction.trace_toEnd_eq_zero, Affine.Simplex.wSameSide_affineSpan_faceOpposite_point_right_iff, Matrix.instLieModuleForall, hasDerivAt_update, OrthonormalBasis.equiv_apply, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_assoc, Matrix.ofLp_toLpLin, Module.Basis.coe_toOrthonormalBasis_repr_symm, LinearMap.det_toLin', groupCohomology.instEpiModuleCatH1π, Module.jacobson_pi_le, hasFDerivAt_list_prod', hasStrictFDerivAt_finCons, groupCohomology.H2π_comp_map, Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, NumberField.mixedEmbedding.mem_span_latticeBasis, OrthonormalBasis.repr_apply_apply, fwdDiff_aux.shiftₗ_pow_apply, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, ContinuousAlternatingMap.hasStrictFDerivAt, hasEigenvector_toLin'_diagonal, groupCohomology.isoCocycles₂_hom_comp_i, UniqueDiffOn.pi, Affine.Simplex.affineCombination_mem_setInterior_face_iff_mem, differentiableOn_pi'', LinearIsometryEquiv.piLpCurry_apply, NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top, groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply, EuclideanSpace.sphere_zero_eq, hasFDerivAt_finCons', instPolynormableSpaceForall, hasStrictFDerivAt_piLp, LinearMap.toMatrix_innerₛₗ_apply, groupCohomology.dArrowIso₀₁_hom_left, Algebra.PreSubmersivePresentation.jacobian_eq_det_aevalDifferential, hasStrictDerivAt_finCons', groupCohomology.cocyclesMap_comp_isoCocycles₁_hom, AffineBasis.toMatrix_vecMul_coords, groupCohomology.eq_d₀₁_comp_inv_apply, hasStrictDerivAt_finCons, PiLp.basisFun_apply, LinearIsometryEquiv.piLpCongrRight_single, groupCohomology.mapCocycles₁_one, finrank_euclideanSpace, Matrix.toLpLin_toLp, ModuleCat.piIsoPi_inv_kernel_ι_apply, hasFDerivAt_list_prod_finRange', CStarMatrix.toCLM_apply_single, PiLp.volume_preserving_ofLp, ContinuousMultilinearMap.hasStrictFDerivAt, Finset.affineCombination_map, AffineBasis.det_smul_coords_eq_cramer_coords, AffineMap.proj_pi, hasFDerivWithinAt_piLp, differentiableOn_piLp, eq_affineCombination_of_mem_affineSpan_of_fintype, AffineBasis.coord_apply_combination_of_notMem, Finset.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one, Module.jacobson_pi_eq_bot, Matrix.ofLp_toEuclideanCLM, CStarMatrix.toCLM_apply_eq_sum, groupCohomology.H2π_comp_map_assoc, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, Finset.affineCombination_indicator_subset, Rep.coindFunctorIso_inv_app_hom_hom_apply_coe, groupCohomology.d₀₁_ker_eq_invariants, AdicCompletion.ofTensorProduct_bijective_of_pi_of_fintype, differentiableAt_finCons, Matrix.toLpLin_symm_id, differentiableWithinAt_euclidean, Matrix.isPositive_toEuclideanLin_iff, NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMap, Affine.Simplex.affineCombination_mem_interior_iff, hasFDerivAt_pi'', groupCohomology.inhomogeneousCochains.d_comp_d, Affine.Simplex.affineCombination_eq_touchpoint_iff, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, Configuration.ofField.instNondegenerateProjectivizationForallFinOfNatNat, Submodule.quotientPi_apply, RootPairing.GeckConstruction.instIsIrreducible, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, differentiableAt_piLp, groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply, groupCohomology.isoCocycles₁_inv_comp_iCocycles, Projectivization.mk_eq_mk_iff_crossProduct_eq_zero, differentiable_pi, CStarMatrix.toCLM_apply, Matrix.charpoly_toLin', deriv_update, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, Finset.affineCombination_linear, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom, Finset.affineCombination_apply, LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply, IccLeftChart_extend_bot, Matrix.l2_opNNNorm_def, Matrix.minpoly_toLin', hasFDerivAt_single, affineCombination_mem_affineSpan_image, groupCohomology.d₁₂_comp_d₂₃_assoc, Finset.affineCombination_affineCombinationLineMapWeights, EuclideanSpace.basisFun_repr, NumberField.mixedEmbedding.span_latticeBasis, FiniteDimensional.finiteDimensional_pi', Finset.affineCombination_filter_of_ne, NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite, Complex.orthonormalBasisOneI_repr_symm_apply, basisFun_det, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, LinearIsometryEquiv.piLpCongrRight_refl, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, WithCStarModule.pi_inner, Matrix.lie_apply, modelWithCornersEuclideanHalfSpace_zero, Rep.coindIso_inv_hom_hom, groupCohomology.subtype_comp_d₀₁_assoc, coe_lpPiLpₗᵢ, AddCommGrpCat.coyonedaType_obj_map, Submodule.pi_liftQ_eq_liftQ_pi, fderiv_update, CStarMatrix.mul_entry_mul_eq_inner_toCLM, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, fwdDiff_aux.fwdDiffₗ_apply, groupCohomology.cocycles₁IsoOfIsTrivial_inv_hom_apply_coe, fwdDiff_aux.shiftₗ_apply, Matrix.charpoly_mulVecLin, Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff, Affine.Simplex.sSameSide_affineSpan_faceOpposite_of_sign_eq, OrthonormalBasis.sum_repr_symm, AddCommGrpCat.HasLimit.productLimitCone_cone_π, orthonormalBasis.toBasis, eq_affineCombination_of_mem_affineSpan, Affine.Simplex.affineCombination_mem_interior_face_iff_pos, WithCStarModule.inner_single_right, groupCohomology.d₁₂_comp_d₂₃, NumberField.Units.instDiscrete_unitLattice, NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, AffineBasis.toMatrix_inv_vecMul_toMatrix, differentiableWithinAt_pi, EuclideanSpace.volume_ball_fin_three, PiLp.projₗ_apply, NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMapBasis, groupCohomology.H1π_eq_zero_iff, groupCohomology.cochainsMap_f, inhomogeneousCochains.d_hom_apply, derivWithin_pi, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_apply, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, OrthonormalBasis.measurePreserving_repr_symm, groupCohomology.cocyclesMk₁_eq, hasStrictFDerivAt_finCons', EuclideanSpace.piLpCongrLeft_single, LinearIsometryEquiv.piLpCurry_symm_apply, hasStrictFDerivAt_list_prod_attach', deriv_single, hasFDerivWithinAt_euclidean, Affine.Simplex.incenter_eq_affineCombination, hasFDerivAt_update, FiniteDimensional.finiteDimensional_pi, UniqueDiffOn.univ_pi, Submodule.quotientPi_symm_apply, hasDerivAtFilter_finCons', groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_apply, Real.map_linearMap_volume_pi_eq_smul_volume_pi, PiLp.hasStrictFDerivAt_apply, Matrix.toEuclideanLin_eq_toLin, groupCohomology.H2π_eq_zero_iff, hasDerivWithinAt_finCons', Euclidean.closedBall_eq_preimage, Matrix.isHermitian_iff_isSymmetric, PiLp.add_apply, groupCohomology.mapCocycles₁_comp_i_assoc, hasStrictFDerivAt_finset_prod, UniqueDiffWithinAt.pi, PiLp.basisFun_eq_pi_basisFun, groupCohomology.H1π_comp_map_apply, MeasureTheory.Measure.map_linearMap_addHaar_pi_eq_smul_addHaar, InnerProductSpace.toMatrix_rankOne, Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iff, differentiableAt_euclidean, hasFDerivAtFilter_finCons, pi_midpoint_apply, groupCohomology.π_comp_H2Iso_hom_assoc, AffineBasis.coords_apply, Submodule.quotientPi_aux.map_add, Matrix.toEuclideanLin_conjTranspose_eq_adjoint, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, Matrix.toLpLinAlgEquiv_apply_apply_ofLp, ContinuousMultilinearMap.iteratedFDerivComponent_apply, Projectivization.orthogonal_mk, EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp, Projectivization.cross_mk, RootPairing.GeckConstruction.f_lie_v_ne, ZLattice.covolume.tendsto_card_le_div, ContinuousMultilinearMap.hasFDerivAt, differentiableOn_euclidean, EuclideanSpace.ball_zero_eq, Affine.Simplex.sOppSide_affineSpan_faceOpposite_of_pos_of_neg, coe_lpPiLpₗᵢ_symm, differentiable_piLp, RootPairing.GeckConstruction.e_lie_v_ne, Matrix.ofLp_toEuclideanLin_apply, EuclideanSpace.volume_ball_fin_two, instIsSemisimpleModuleForallOfFinite, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_assoc, lieEquivMatrix'_symm_apply, Euclidean.ball_eq_preimage, EuclideanSpace.volume_ball, OrthonormalBasis.repr_symm_single, groupCohomology.eq_d₂₃_comp_inv, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, Affine.Simplex.point_eq_affineCombination_of_pointsWithCircumcenter, ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap, Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype, ProbabilityTheory.iIndepFun_iff_charFunDual_pi', ModuleCat.piIsoPi_hom_ker_subtype_apply, groupCohomology.isoCocycles₂_inv_comp_iCocycles, toMatrix_innerSL_apply, Module.length_pi_of_fintype, AffineMap.pi_comp, PiLp.basis_toMatrix_basisFun_mul, mapsTo_tangentConeAt_pi, affineCombination_mem_convexHull, inhomogeneousCochains.d_eq, ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear, ModuleCat.piIsoPi_hom_ker_subtype, groupCohomology.cocyclesMk₂_eq, Finset.weightedVSub_vadd_affineCombination, PiLp.hasFDerivAt_ofLp, affineCombination_mem_affineSpan_of_nonempty, UniqueDiffWithinAt.univ_pi, ModuleCat.piIsoPi_inv_kernel_ι, differentiableAt_finCons', Submodule.quotientPi_aux.left_inv, Affine.Simplex.centroid_eq_affineCombination, groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply, MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux, Affine.Simplex.sSameSide_affineSpan_faceOpposite_point_right_iff, withSeminorms_pi, groupCohomology.isoCocycles₁_hom_comp_i, AddCommGrpCat.biproductIsoPi_inv_comp_π, Affine.Simplex.affineCombination_touchpointWeights, hasDerivAtFilter_finCons, Matrix.toPerfectPairing, det_fderivPiPolarCoordSymm, groupCohomology.mapCocycles₁_comp_i_apply, Rep.coindMap_hom, InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular', NumberField.mixedEmbedding.hasFDerivAt_polarCoordReal_symm, hasEigenvalue_toLin'_diagonal_iff, Matrix.toLpLin_mul, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃, MeasureTheory.charFunDual_eq_pi_iff', AddCommGrpCat.HasLimit.lift_hom_apply, hasFDerivAt_pi_polarCoord_symm, coe_addEquiv_lpPiLp, mem_fintypeAffineCoords_iff_sum, Matrix.toEuclideanLin_apply_piLp_toLp, Finset.attach_affineCombination_of_injective, hasStrictDerivAt_pi, groupCohomology.cochainsMap_f_hom, WithCStarModule.inner_single_left, AffineMap.pi_eq_zero, RootPairing.GeckConstruction.lie_e_lie_f_apply, groupCohomology.π_comp_H2Iso_hom_apply, hasFDerivWithinAt_pi, ModuleCat.HasLimit.lift_hom_apply, stdSimplex.barycenter_eq_centerMass, differentiableWithinAt_apply, ContinuousAlternatingMap.hasFDerivWithinAt, PiLp.hasFDerivAt_apply, volume_euclideanSpace_eq_dirac, Projectivization.cross_mk_of_ne, QuadraticMap.Ring.associated_pi, Affine.Simplex.affineCombination_mem_closedInterior_face_iff_mem_Icc, Module.Injective.pi, OrthonormalBasis.coe_toBasis_repr, hasStrictFDerivAt_list_prod, hasDerivAtFilter_pi, PiLp.proj_apply, groupCohomology.π_comp_H1Iso_hom_apply, OrthonormalBasis.sum_repr, groupCohomology.d₀₁_comp_d₁₂_assoc, Matrix.toLpLin_symm_comp, RootPairing.GeckConstruction.f_lie_v_same, hasDerivAt_finCons', LinearIsometryEquiv.piLpCongrLeft_single, NumberField.Units.unitLattice_rank, Submodule.quotientPiLift_mk, differentiable_pi'', hasDerivAt_single, OrthonormalBasis.coe_toBasis_repr_apply, affineCombination_eq_centerMass, PiLp.neg_apply, PiLp.coe_symm_continuousLinearEquiv, differentiableOn_apply, ModuleCat.biproductIsoPi_inv_comp_π_apply, differentiableAt_pi, AffineIndependent.injOn_affineCombination_fintypeAffineCoords, ZSpan.discreteTopology_pi_basisFun, Affine.Simplex.signedInfDist_affineCombination, NumberField.Units.logEmbeddingEquiv_apply, ModuleCat.HasLimit.productLimitCone_cone_pt_isAddCommGroup, EuclideanGeometry.dist_affineCombination, groupCohomology.d₀₁_comp_d₁₂_apply, Finset.sum_smul_vsub_const_eq_affineCombination_vsub, hasFDerivAtFilter_finCons', groupCohomology.cocyclesIso₀_hom_comp_f_apply, Submodule.quotientPi_aux.right_inv, groupCohomology.subtype_comp_d₀₁, AdicCompletion.piEquivOfFintype_apply, Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_right_iff, tendsto_card_div_pow_atTop_volume', fromModuleCatToModuleCatLinearEquiv_apply, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, fromModuleCatToModuleCatLinearEquiv_symm_apply_coe, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, LinearMap.det_toMatrix', ContinuousAlternatingMap.differentiable, NumberField.mixedEmbedding.euclidean.finrank, Module.length_pi, AffineBasis.affineCombination_coord_eq_self, PiLp.zero_apply, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_assoc, Finset.sum_smul_vsub_eq_affineCombination_vsub, groupCohomology.isoCocycles₂_hom_comp_i_apply, hasStrictFDerivAt_list_prod', AffineMap.pi_zero, AffineBasis.coord_apply_combination_of_mem, Projectivization.cross_mk_of_cross_eq_zero, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, fwdDiff_aux.coe_fwdDiffₗ_pow, differentiableWithinAt_piLp, PiLp.hasStrictFDerivAt_ofLp, groupCohomology.H1π_comp_map, NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm, Matrix.cstar_norm_def, differentiable_finCons, PiLp.basisFun_map, AffineIndependent.affineCombination_eq_lineMap_iff_weight_lineMap, Configuration.ofField.mem_iff, Quaternion.linearIsometryEquivTuple_apply, PiLp.continuousLinearEquiv_apply, Matrix.maxGenEigenspace_toLin'_diagonal_eq_eigenspace, hasStrictFDerivAt_pi'', Module.Finite.exists_fin_quot_equiv, groupCohomology.isoShortComplexH1_inv, ContinuousAlternatingMap.hasFDerivAt, Matrix.toLpLin_apply, differentiableOn_finCons, Module.pi_induction', hasDerivAt_pi, Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, hasDerivWithinAt_finCons, EuclideanSpace.single_eq_zero_iff, weightedVSub_mem_vectorSpan_pair, QuadraticMap.Ring.polar_pi, fderiv_pi, Matrix.l2_opNorm_def, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁, Matrix.toEuclideanLin_toLp, LinearIsometryEquiv.piLpCongrLeft_symm, OrthonormalBasis.measurePreserving_measurableEquiv, TannakaDuality.FiniteGroup.ofRightFDRep_hom, groupCohomology.eq_d₁₂_comp_inv_assoc, Affine.Simplex.affineCombination_mem_setInterior_iff, orthonormalBasis_repr, fwdDiff_aux.coe_fwdDiffₗ, AffineMap.pi_linear, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, hasFDerivAtFilter_pi', ModuleCat.HasLimit.productLimitCone_isLimit_lift, IccRightChart_extend_top, Matrix.toLpLinAlgEquiv_symm_apply, groupCohomology.isoShortComplexH2_inv, groupCohomology.isoCocycles₂_hom_comp_i_assoc, Rep.coindIso_hom_hom_hom, Finset.centroid_def, hasFDerivAt_pi', Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff, ContinuousMultilinearMap.hasStrictFDerivAt_uncurry, PiLp.instIsBoundedSMul, groupCohomology.coe_mapCocycles₂, groupCohomology.eq_d₀₁_comp_inv_assoc, AdicCompletion.piEquivFin_apply, EuclideanSpace.volume_closedBall, fderiv_single, finrank_euclideanSpace_fin, Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter, hasFDerivAt_list_prod_attach', groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_assoc, groupCohomology.H1π_eq_iff, OrthonormalBasis.repr_reindex, InnerProductSpace.symm_toEuclideanLin_rankOne, groupCohomology.isoCocycles₁_hom_comp_i_assoc, hasStrictFDerivAt_pi, Affine.Simplex.faceOppositeCentroid_eq_affineCombination, Finset.affineCombination_subtype_eq_filter, Matrix.rank_vecMulVec, hasDerivAt_finCons, OrthonormalBasis.tensorProduct_repr_tmul_apply, convexHull_range_eq_exists_affineCombination, Matrix.toLpLin_eq_toLin, PiLp.sumPiLpEquivProdLpPiLp_apply_ofLp, groupCohomology.mapCocycles₁_comp_i, RootPairing.GeckConstruction.e_lie_u, CStarMatrix.norm_def, AddCommGrpCat.coyonedaType_map_app, groupCohomology.cocycles₁.d₁₂_apply, Int.submodule_toAddSubgroup_index_ne_zero_iff, basisFun_det_apply, groupCohomology.π_comp_H2Iso_hom, hasFDerivAt_pi, differentiableWithinAt_finCons, BoxIntegral.unitPartition.tag_mem_smul_span, parallelepiped_single, hasFDerivWithinAt_apply, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, CStarMatrix.inner_toCLM_conjTranspose_right, LieModule.toEnd_matrix, ZLattice.covolume_eq_det, CStarMatrix.toCLM_apply_single_apply, Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_left_iff, PiLp.hasStrictFDerivAt_toLp, groupCohomology.d₀₁_eq_zero, Matrix.spectrum_toLin', hasStrictFDerivAt_euclidean, hasFDerivAt_finset_prod
addCommMonoid 📖	CompOp	1492 math math: ArithmeticFunction.vonMangoldt.residueClass_eq, comul_eq_adjoint, Matrix.UnitaryGroup.toLin'_one, Rep.resCoindHomEquiv_symm_apply_hom, Finset.weightedVSub_sdiff, Rep.resCoindHomEquiv_apply_hom, groupCohomology.instEpiModuleCatH2π, ContinuousLinearMap.sum_comp_single, PiLp.continuousLinearEquiv_symm_apply, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, Lagrange.interpolate_one, rank_fun_infinite, Finset.weightedVSubOfPoint_map, Algebra.SubmersivePresentation.cotangentComplexAux_injective, Module.Basis.equivFun_self, MeasureTheory.eLpNorm'_sum_le, exists_continuous_sum_one_of_isOpen_isCompact, iSupIndep.dfinsupp_lsum_injective, dot_self_cross, Finset.affineCombination_vsub, DFinsupp.lsum_lsingle, Lagrange.interpolate_eq_of_values_eq_on, Matrix.toLin'_symm, QuaternionAlgebra.coe_linearEquivTuple_symm, Matrix.SeparatingLeft.toBilin', AddSubmonoid.IsLocalizationMap.pi, cfc_sum_univ, NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, IsIsotypic.linearEquiv_fun, LinearMap.toMatrixAlgEquiv'_mul, Polynomial.ofFn_zero, groupCohomology.toCocycles_comp_isoCocycles₁_hom, Module.Basis.map_equivFun, HasDerivAtFilter.sum, groupCohomology.isoCocycles₁_hom_comp_i_apply, MultilinearMap.fromDFinsuppEquiv_apply, LinearMap.funLeft_id, groupCohomology.mem_cocycles₂_def, LinearMap.toAddMonoidHom_proj, NumberField.Units.finrank_eq_rank, TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, SimpleGraph.lapMatrix_toLinearMap₂', tendsto_tsum_div_pow_atTop_integral, NumberField.canonicalEmbedding.mem_span_latticeBasis, hasStrictFDerivAt_list_prod_finRange', Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, NumberField.Units.logEmbedding_fundSystem, dotProductEquiv_symm_apply, LSeries.term_sum, LinearEquiv.piCongrRight_apply, Matrix.separatingRight_toLinearMap₂'_iff, ZSpan.volume_real_fundamentalDomain, image_update_openSegment, Lagrange.eval_interpolate_not_at_node', Matrix.det_smul_inv_mulVec_eq_cramer, Matrix.UnitaryGroup.toGL_mul, ContinuousMultilinearMap.norm_iteratedFDerivComponent_le, Finset.weightedVSubOfPoint_apply, IntervalIntegrable.sum, Matrix.toLinearMapRight'_mul, Submodule.fg_pi, hasFDerivAt_multiset_prod, Module.Basis.equivFun_symm_apply, MeasureTheory.Submartingale.sum_mul_sub', Nat.isLinearSet_iff_exists_matrix, LinearMap.ker_pi, Matrix.cramer_transpose_row_self, NumberField.canonicalEmbedding.latticeBasis_apply, Matrix.iSup_eigenspace_toLin'_diagonal_eq_top, AlternatingMap.coe_pi, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, QuadraticMap.posDef_pi_iff, groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply, Module.Basis.constr_comp, Module.Basis.constr_symm_apply, Finsupp.sum_apply', Rep.resCoindAdjunction_counit_app_hom_hom, IsAdjoinRootMonic.coeff_apply, Matrix.toLinearMap₂'_comp, Matrix.l2_opNorm_mulVec, Finset.weightedVSubOfPoint_insert, Representation.finsupp_apply, groupCohomology.H1π_comp_map_assoc, ZMod.LFunction_one_sub, ceilDiv_def, groupCohomology.π_comp_H1Iso_hom_assoc, MDifferentiableAt.sum, TensorProduct.sum_tmul_basis_right_injective, Ideal.map_pi, ZMod.dft_even_iff, comul_comp_dFinsuppCoeFnLinearMap, Finset.affineCombination_sdiff_sub, ZMod.invDFT_apply, RCLike.linearIndependent_of_ne_zero_of_wInner_one_eq_zero, Matrix.liftLinear_single, counit_coe_dFinsupp, TensorProduct.piScalarRight_symm_algebraMap, ContinuousAlternatingMap.opNNNorm_pi, LinearMap.BilinForm.toMatrix_basisFun, Rep.indToCoindAux_self, groupCohomology.mapCocycles₂_comp_i, LinearMap.det_pi, NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm, Matrix.vec_sum, ProbabilityTheory.iIndepFun.mgf_sum₀, Finset.weightedVSubOfPoint_congr, Rep.diagonalHomEquiv_symm_apply, cross_cross, QuadraticMap.Isometry.proj_comp_single_of_same, IsBaseChange.of_fintype_basis_eq, FunOnFinite.linearMap_comp, Finsupp.linearEquivFunOnFinite_symm_coe, LinearEquiv.piCongrRight_trans, Multiset.aemeasurable_sum, stdSimplex_fin_two, NumberField.mixedEmbedding.mem_idealLattice, BoxIntegral.unitPartition.mem_smul_span_iff, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, LinearMap.BilinForm.toMatrix'_symm, Matrix.cramer_row_self, groupCohomology.coe_mapCocycles₁, linearIndependent_single, UniformOnFun.ofFun_sum, MultilinearMap.piFamily_add, PiToModule.fromEnd_apply, locallyConvexSpace, Submodule.pi_univ_bot, LinearMap.BilinForm.toMatrix'_apply, ContinuousAlternatingMap.piLIE_apply_apply, QuadraticMap.Isometry.single_apply, AdicCompletion.incl_apply, convex_pi, ModuleCat.instSmallSubtypeForallCarrierObjMemSubmoduleSectionsSubmodule, LinearMap.nondegenerate_toLinearMap₂'_of_det_ne_zero', fourierCoeff.sum, ZMod.dft_mul_const, cross_self, groupCohomology.coboundariesToCocycles₁_apply, Submodule.quotientPi_aux.map_smul, Lagrange.eval_interpolate_not_at_node, Matrix.blockDiagonal_tsum, ContinuousMultilinearMap.piLinearEquiv_symm_apply, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, Matrix.intrinsicStar_toLin', MeasureTheory.Submartingale.sum_sub_upcrossingStrat_mul, ContinuousAlternatingMap.coe_pi, Finset.univ_sum_single, Polynomial.ofFn_eq_sum_monomial, Matrix.coe_mulVecLin, Matrix.mulVecLin_apply, continuous_equivFun_basis, ExteriorAlgebra.liftAlternating_ι_mul, Lagrange.interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C, MDifferentiable.sum, fwdDiff_finset_sum, Fintype.linearIndependent_iff', Algebra.TensorProduct.piRightHom_mul, Module.le_rank_iff_exists_linearMap, Lagrange.interpolate_eq_sum_interpolate_insert_sdiff, QuadraticMap.toMatrix'_comp, HasFDerivWithinAt.continuousMultilinearMapCompContinuousLinearMap, LinearEquiv.piFinTwo_symm_apply, Matrix.GeneralLinearGroup.coe_toLin, SimpleGraph.card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix, Finset.weightedVSub_apply_const, star_dotProduct_toMatrix₂_mulVec, isStablyFiniteRing_iff_injective_of_surjective, IsLocalFrameOn.coeff_apply_of_mem, Finset.weightedVSubOfPoint_indicator_subset, Submodule.iSup_map_single_le, range_vecMulLinear, comul_comp_single, MeasureTheory.Submartingale.sum_upcrossingStrat_mul, groupCohomology.mem_cocycles₁_of_addMonoidHom, NumberField.mixedEmbedding.commMap_apply_of_isComplex, groupCohomology.cocycles₂.d₂₃_apply, LinearMap.spectrum_toMatrix', LinearMap.iSup_range_single, Real.smul_map_diagonal_volume_pi, Algebra.TensorProduct.piScalarRight_tmul, ContinuousLinearMap.single_apply, MeasureTheory.BorelCantelli.martingalePart_process_ae_eq, Matrix.diagLinearMap_apply, Matrix.diagonalLinearMap_apply, extremePoints_pi, fderiv_sum, strongRankCondition_iff_forall_not_injective, dot_cross_self, Algebra.PreSubmersivePresentation.isUnit_jacobian_iff_aevalDifferential_bijective, QuadraticAlgebra.linearEquivTuple_apply, QuadraticForm.equivalent_signType_weighted_sum_squared, Real.circleAverage_sum, Finset.weightedVSub_map, Summable.matrix_blockDiag, Matrix.linearIndependent_rows_of_invertible, LinearEquiv.piCurry_apply, Matrix.coe_vecMulLinear, counit_comp_finsuppLcoeFun, Matrix.SeparatingLeft.toLinearMap₂', Finsupp.llift_apply, ExteriorAlgebra.liftAlternating_comp, LDL.lowerInv_eq_gramSchmidtBasis, LinearMap.iInf_ker_proj, hasStrictFDerivAt_pi', HasFDerivAt.continuousMultilinearMapCompContinuousLinearMap, Matrix.sum_cramer, mem_vectorSpan_iff_eq_weightedVSub, MeromorphicOn.extract_zeros_poles_log, mem_convexHull_pi, Fintype.bilinearCombination_apply_single, LinearMap.toMatrixₛₗ₂'_symm, PiLp.coe_continuousLinearEquiv, BoxIntegral.hasIntegral_GP_pderiv, ContinuousMultilinearMap.linearDeriv_apply, QuadraticMap.discr_smul, dotProductEquiv_apply_apply, LinearMap.rank_diagonal, DifferentiableWithinAt.sum, NumberField.mixedEmbedding.negAt_apply_snd, LinearMap.separatingRight_toMatrix₂'_iff, Submodule.biSup_eq_range_dfinsupp_lsum, Rep.resCoindAdjunction_unit_app_hom_hom, groupCohomology.mem_cocycles₁_def, ContinuousAlternatingMap.piEquiv_apply, IsIsotypic.submodule_linearEquiv_fun, hasFDerivWithinAt_pi', LinearMap.toMatrixAlgEquiv'_id, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, CuspForm.coe_trace, BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt, Matrix.liftLinear_singleLinearMap, ExpGrowth.expGrowthSup_sum, Fin.consEquivL_apply, NumberField.mixedEmbedding.negAt_preimage, Matrix.liftLinear_comp_singleLinearMap, QuadraticForm.equivalent_one_neg_one_weighted_sum_squared, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, LinearMap.toMatrix₂'_compl₁₂, groupCohomology.mapCocycles₂_comp_i_apply, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_apply, MeasureTheory.charFunDual_pi', NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, Matrix.sum_vecMul, BoxIntegral.unitPartition.integralSum_eq_tsum_div, LinearMap.iInf_ker_proj_le_iSup_range_single, Submodule.mem_pi, Matrix.toLinearEquivRight'OfInv_symm_apply, counit_eq_adjoint, AdicCompletion.pi_apply_coe, Matrix.toLin'_mul_apply, MultilinearMap.fromDirectSumEquiv_symm_apply, ProbabilityTheory.iIndepFun.indepFun_sum_range_succ₀, Finset.sum_smul_vsub_eq_weightedVSubOfPoint_sub, Matrix.toLinearMapₛₗ₂'_single, Matrix.nondegenerate_toBilin'_iff, Lagrange.eq_interpolate_iff, compRightL_apply, groupCohomology.coboundaries₁_eq_bot_of_isTrivial, ContinuousLinearMapWOT.inducingFn_apply, segment_single_subset_stdSimplex, DFinsupp.injective_pi_lapply, linearIndependent_monoidHom, LinearMap.toMatrix'_toLin', tendsto_card_div_pow_atTop_volume, DFinsupp.range_mapRangeLinearMap, counit_comp_dFinsuppCoeFnLinearMap, linearIndependent_single_of_ne_zero, NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd, Matrix.toLinearMap₂'_apply', ContinuousLinearMap.pi_apply, Finset.sum_indicator_mod, Finset.weightedVSubOfPoint_vadd, PiToModule.fromEnd_injective, groupCohomology.cocycles₂_map_one_fst, SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable, NumberField.mixedEmbedding.negAt_signSet_apply_isComplex, groupCohomology.mapCocycles₂_comp_i_assoc, LinearEquiv.coe_curry, Matrix.ker_mulVecLin_conjTranspose_mul_self, groupCohomology.H1IsoOfIsTrivial_inv_apply, FirstOrder.Field.lift_genericMonicPoly, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, Matrix.mulVecLin_add, Matrix.linearIndependent_cols_of_isUnit, basis_repr_single, ContinuousLinearEquiv.piUnique_symm_apply, AddMonoidHom.coe_dfinsuppSumAddHom, LinearMap.funLeft_comp, intrinsicStar_comul_commSemiring, AddCommMonCat.coyonedaType_obj_map, hasStrictFDerivAt_multiset_prod, Module.Basis.ofEquivFun_repr_apply, fwdDiff_iter_finset_sum, groupCohomology.mem_cocycles₁_of_comp_eq_d₀₁, NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm, Module.Free.pi, groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, Lagrange.interpolate_eq_sum, Matrix.SpecialLinearGroup.toLin'_symm_to_linearMap, Matrix.toLinearMap₂'Aux_single, groupCohomology.H2π_comp_map_apply, Matrix.vecMulBilin_apply, Matrix.instSMulCommClassForall_1, cross_anticomm, HasFDerivAt.sum, RootPairing.Base.exists_mem_span_pairingIn_ne_zero_and_pairwise_ne, cross_cross_eq_smul_sub_smul, Real.map_matrix_volume_pi_eq_smul_volume_pi, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply, ContinuousLinearEquiv.finTwoArrow_symm_apply, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, Finset.weightedVSubOfPoint_filter_of_ne, QuadraticMap.Ring.polarBilin_pi, ContinuousLinearMap.det_pi, PiLp.sumPiLpEquivProdLpPiLp_symm_apply_ofLp, TensorProduct.equivFinsuppOfBasisLeft_symm, groupCohomology.toCocycles_comp_isoCocycles₂_hom, Module.Basis.coe_toOrthonormalBasis_repr, ContinuousLinearMap.iInf_ker_proj, DirectSum.ker_lmap, Matrix.piRingEquiv_apply, ExteriorAlgebra.liftAlternatingEquiv_symm_apply, Matrix.toLinearMap₂'_apply, LinearMap.funLeft_surjective_of_injective, AddCommMonCat.coyonedaType_map_app, hasFDerivAt_finCons, LinearMap.BilinForm.separatingLeft_toMatrix'_iff, Matrix.linfty_opNNNorm_eq_opNNNorm, ModularGroup.lcRow0Extend_symm_apply, ZLattice.covolume.tendsto_card_div_pow, hasFDerivWithinAt_finCons, dotProduct_sum, MeasureTheory.BorelCantelli.predictablePart_process_ae_eq, groupCohomology.cocyclesOfIsCocycle₁_coe, Matrix.isNilpotent_toLin'_iff, Module.Basis.constrL_apply, Finset.sum_apply, IsModuleTopology.continuous_bilinear_of_pi_fintype, Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero, IsLocalFrameOn.coeff_congr, groupCohomology.coboundaries₂_le_cocycles₂, NumberField.Units.span_basisOfIsMaxRank, Matrix.toLinearEquiv'_symm_apply, MeasureTheory.Submartingale.sum_mul_sub, LinearMap.BilinForm.mul_toMatrix'_mul, ContinuousLinearEquiv.piUnique_apply, ProbabilityTheory.covariance_sum_right', MultilinearMap.coe_sum, Finset.weightedVSub_empty, NumberField.canonicalEmbedding.integralBasis_repr_apply, InnerProductGeometry.norm_toLp_symm_crossProduct, isNoetherian_linearMap_pi, Finsupp.lcoeFun_comp_lsingle, FunOnFinite.continuous_linearMap, NumberField.Units.basisOfIsMaxRank_apply, Rep.coindVEquiv_symm_apply_coe, ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_sum_of_notMem₀, ContinuousLinearMap.proj_apply, MeromorphicAt.sum, Finsupp.lcoeFun_apply, Module.Finite.exists_nat_not_surjective, groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply, ExteriorAlgebra.liftAlternating_ιMulti, NumberField.mixedEmbedding.negAt_signSet_apply_isReal, Matrix.cramer_apply, LinearMap.lsum_apply, eventuallyEq_sum, LinearEquiv.funUnique_symm_apply, Matrix.toLinearMapₛₗ₂'_symm, Matrix.cRank_toNat_eq_finrank, ProbabilityTheory.covariance_sum_right, summable_matrix_diagonal, groupCohomology.coboundaries₂.val_eq_coe, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, convexHull_basis_eq_stdSimplex, basis_apply, Matrix.piRingEquiv_symm_apply, MeasureTheory.stoppedValue_eq, LinearMap.toBilin'Aux_toMatrixAux, Finset.weightedVSub_weightedVSubVSubWeights, Matrix.linearIndependent_cols_of_det_ne_zero, finsum_apply, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_eq, Matrix.piLinearEquiv_apply, AdicCompletion.val_sum, ZMod.dft_comp_unitMul, Finset.weightedVSubOfPoint_sdiff, DFinsupp.sum_mapRange_index.linearMap, ProbabilityTheory.Kernel.iIndepFun.indepFun_sum_range_succ, Ideal.pi_mkQ_surjective, ExteriorAlgebra.liftAlternatingEquiv_apply, LinearMap.iSup_range_single_eq_iInf_ker_proj, groupCohomology.d₁₂_apply_mem_cocycles₂, Matrix.det_updateRow_sum_aux, groupCohomology.d₀₁_apply_mem_cocycles₁, LinearMap.proj_apply, Matrix.toLinearMapₛₗ₂'_aux_eq, stdSimplex.map_coe, MeasureTheory.condExp_finset_sum, Rep.indToCoindAux_fst_mul_inv, Matrix.ker_mulVecLin_eq_bot_iff, Matrix.linfty_opNNNorm_toMatrix, Module.Basis.coe_constrL, strongRankCondition_iff_forall_rank_lt_aleph0, Submodule.biInf_comap_proj, Multiset.periodic_sum, ContinuousLinearMap.pi_eq_zero, ContinuousLinearMap.pi_proj, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, ContinuousAlternatingMap.piEquiv_symm_apply, ZSpan.volume_fundamentalDomain, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice, basis_toMatrix_basisFun_mul, cross_anticomm', groupCohomology.H2π_eq_iff, toBilin'Aux_toMatrixAux, intrinsicStar_comul, Finsupp.linearEquivFunOnFinite_symm_apply, Finset.periodic_sum, BilinForm.dotProduct_toMatrix_mulVec, LinearEquiv.piUnique_symm_apply, PiLp.hasFDerivAt_toLp, Finset.eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype, QuadraticMap.proj_apply, Projectivization.cross_mk_of_cross_ne_zero, groupCohomology.cocycles₂_map_one_snd, AddMonoidHom.coe_finset_sum, LinearRecurrence.solSpace_rank, TannakaDuality.FiniteGroup.sumSMulInv_apply, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, translate_sum_right, Matrix.piLp_ofLp_toEuclideanLin, LinearEquiv.piUnique_apply, LinearEquiv.sumPiEquivProdPi_apply, multiset_sum_apply, PowerBasis.constr_pow_algebraMap, AnalyticOnNhd.eval_linearMap, lieEquivMatrix'_apply, hasFTaylorSeriesUpToOn_pi', Differentiable.sum, Matrix.toPerfectPairing_apply_apply, Matrix.mulVecLin_zero, SimpleGraph.linearIndependent_lapMatrix_ker_basis_aux, FunOnFinite.linearMap_apply_apply, Rep.indToCoindAux_comm, LinearEquiv.sumArrowLequivProdArrow_symm_apply_inr, instFinitePresentationForall, LinearEquiv.funCongrLeft_apply, groupCohomology.π_comp_H1Iso_hom, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, LinearMap.minpoly_toMatrix', cfcₙ_sum_univ, Matrix.linearIndependent_rows_of_isUnit, isOrderedAddCancelMonoid, Fintype.bilinearCombination_apply, Matrix.l2_opNNNorm_mulVec, NumberField.mixedEmbedding.span_idealLatticeBasis, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, Lagrange.degree_interpolate_erase_lt, Matrix.SeparatingRight.toLinearMap₂', Submodule.mem_iSup_iff_exists_dfinsupp, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv, PointwiseConvergenceCLM.isInducing_inducingFn, ValueDistribution.proximity_sum_top_le, iteratedDerivWithin_sum, HasSum.matrix_blockDiag', LinearMap.BilinForm.separatingRight_toMatrix'_iff, Matrix.isUnit_toLin'_iff, Module.piEquiv_apply_apply, sum_dotProduct, HasStrictDerivAt.sum, IsIsotypicOfType.linearEquiv_fun, Finset.weightedVSub_smul, Matrix.toLin'_mul, Submodule.iSup_eq_range_dfinsupp_lsum, ModularGroup.lcRow0Extend_apply, LinearMap.BilinForm.dotProduct_toMatrix_mulVec, Lagrange.degree_interpolate_lt, ExteriorAlgebra.liftAlternating_apply_ιMulti, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_assoc, Matrix.Module.smul_def, LinearMap.vecCons_apply, Matrix.ofLp_toLpLin, Module.range_piEquiv, Matrix.toMatrix₂Aux_toLinearMap₂'Aux, Matrix.toBilin'_symm, Module.Basis.dualBasis_equivFun, ProbabilityTheory.covariance_sum_left, Representation.coe_coindV, Module.Basis.coe_toOrthonormalBasis_repr_symm, ProbabilityTheory.mgf_sum_of_identDistrib₀, RootPairing.EmbeddedG2.allRoots_eq_map_allCoeffs, VertexOperator.ncoeff_apply, Matrix.one_vecMul, MeasureTheory.withDensity_tsum, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, Matrix.mulVecLin_one, MultilinearMap.fromDFinsuppEquiv_single, LinearMap.det_toLin', MvPolynomial.map_restrict_dom_evalₗ, groupCohomology.instEpiModuleCatH1π, LinearMap.mapMatrixModule_apply, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_eq, Module.FinitePresentation.exists_fin, Submodule.pi_mono, Ideal.pi_tensorProductMk_quotient_surjective, hasFDerivAt_list_prod', Matrix.toLinearMapRight'_mul_apply, hasStrictFDerivAt_finCons, groupCohomology.H2π_comp_map, Matrix.eRank_toNat_eq_finrank, Matrix.mulVec_sum, circleIntegrable_log_norm_factorizedRational, Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, LinearMap.coe_proj, NumberField.mixedEmbedding.mem_span_latticeBasis, Module.Basis.equivFunL_symm_apply_repr, Rep.coindToInd_apply, pi_eq_sum_univ', HasFDerivAtFilter.sum, fwdDiff_aux.shiftₗ_pow_apply, Submodule.pi_empty, Finsupp.lsum_single, QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared, Finsupp.linearEquivFunOnFinite_single, LinearMap.separatingLeft_toMatrix₂'_iff, QuadraticForm.equivalent_weightedSumSquares, TannakaDuality.FiniteGroup.leftRegular_apply, ContinuousMap.coeFnLinearMap_apply, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, LinearMap.pi_apply, Matrix.cramer_zero, hasEigenvector_toLin'_diagonal, Matrix.GeneralLinearGroup.toLin'_apply, LinearMap.mapMatrixModule_id_apply, Finset.stronglyMeasurable_sum, LinearMap.toMatrixAlgEquiv'_apply, Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin, groupCohomology.isoCocycles₂_hom_comp_i, NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem, BoundedContinuousFunction.coe_sum, ContinuousLinearMapWOT.isInducing_inducingFn, Matrix.vecMulLinear_apply, Matrix.toLinearMapₛₗ₂'_toMatrix', LinearMap.pi_eq_zero, LinearMap.toMatrix'_algebraMap, Matrix.cramer_reindex, ProbabilityTheory.iIndepFun.integrable_exp_mul_sum, PiToModule.fromMatrix_apply_single_one, Matrix.det_updateRow_sum, NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top, SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux, groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply, cfc_sum, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_eq, NumberField.mixedEmbedding.volume_preserving_negAt, MeasureTheory.memLp_finset_sum', IsBaseChange.of_fintype_basis, LinearEquiv.piRing_symm_apply, TensorProduct.piRight_symm_apply, MeasureTheory.uniformIntegrable_average_real, LinearMap.funLeft_injective_of_surjective, NumberField.mixedEmbedding.negAt_apply_isComplex, IsLocalizedModule.pi, Matrix.toBilin_basisFun, Matrix.ker_mulVecLin_transpose_mul_self, Matrix.toLin'_reindex, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom, ContinuousLinearEquiv.finTwoArrow_apply, Matrix.PosSemidef.toLinearMap₂'_zero_iff, LinearMap.BilinForm.toMatrix'_compLeft, MultilinearMap.map_add_sub_map_add_sub_linearDeriv, Matrix.vecMul_eq_sum, Matrix.diag_multiset_sum, Module.finrank_pi, span_range_eq_top_iff_surjective_fintypeLinearCombination, ContinuousMultilinearMap.piLinearEquiv_apply, NumberField.mixedEmbedding.normAtComplexPlaces_normAtAllPlaces, LSeriesSummable.sum, ExteriorAlgebra.liftAlternating_one, DirectSum.linearEquivFunOnFintype_lof, groupCohomology.cocycles₁_map_inv, Rep.freeLiftLEquiv_apply, Submodule.set_smul_eq_map, Multiset.stronglyMeasurable_sum, groupCohomology.mapCocycles₁_one, ProbabilityTheory.iIndepFun.cgf_sum, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply, LinearMap.BilinForm.nondegenerate_toBilin'_iff_det_ne_zero, LinearMap.toMatrix'_apply, Matrix.toLpLin_toLp, ProbabilityTheory.covariance_sum_sum, Rep.indToCoindAux_mul_fst, Matrix.rank_eq_finrank_span_row, MultilinearMap.freeDFinsuppEquiv_def, summable_matrix_blockDiagonal', Lagrange.eq_interpolate, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_apply, ZMod.invDFT_def', NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem, ContinuousLinearMap.continuousMultilinearMapOption_apply_eq_self, NumberField.Units.regOfFamily_of_isMaxRank, Module.Basis.equivFunL_apply, Matrix.IntrinsicStar.isSelfAdjoint_toLin'_iff, hasFDerivAt_list_prod_finRange', Fintype.linearIndependent_iff'ₛ, TensorProduct.piRight_symm_single, ContinuousLinearMap.coe_pi, ContinuousMultilinearMap.pi_apply, AffineBasis.det_smul_coords_eq_cramer_coords, Submodule.pi_top, ContinuousLinearMapWOT.isEmbedding_inducingFn, HasSum.matrix_diag, LinearMap.toMatrix'_symm, InnerProductGeometry.norm_ofLp_crossProduct, LinearMap.coe_sum, MeasureTheory.stoppedProcess_eq, groupCohomology.mem_cocycles₂_iff, Matrix.range_mulVecLin, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_increments, DFinsupp.linearEquivFunOnFintype_symm_apply, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply, basis_repr, MeasureTheory.Submartingale.sum_mul_upcrossingStrat_le, groupCohomology.H2π_comp_map_assoc, Summable.matrix_blockDiag', NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, ProbabilityTheory.iIndepFun.indepFun_sum_range_succ, ProbabilityTheory.Kernel.withDensity_tsum, Matrix.range_toLin', RootPairing.GeckConstruction.span_range_h_le_range_diagonal, Summable.matrix_diag, LinearEquiv.finTwoArrow_apply, LinearMap.pi_apply_eq_sum_univ, ContinuousMultilinearMap.opNorm_pi, ZMod.dft_apply, Rep.coindFunctorIso_inv_app_hom_hom_apply_coe, LinearMap.mul_toMatrix', Matrix.liftLinear_apply, LinearMap.toMatrix₂_basisFun, QuadraticMap.Isometry.proj_comp_single_of_ne, IsBaseChange.pi, HVertexOperator.of_coeff_coeff, Polynomial.toFn_zero, Polynomial.ofFn_zero', Matrix.mul_adjugate_apply, IsLocalFrameOn.eventually_eq_sum_coeff_smul, ProbabilityTheory.iCondIndepFun.condIndepFun_finset_sum_of_notMem, HVertexOperator.coeff_inj_iff, Matrix.toBilin'Aux_single, MDifferentiableOn.sum, QuadraticMap.discr_comp, LinearMap.coeFn_sum, groupCohomology.mem_cocycles₁_iff, LinearMap.lsum_single, Matrix.sum_cramer_apply, ZMod.invDFT_apply', Matrix.UnitaryGroup.coe_toGL, Matrix.linearIndependent_cols_iff_isUnit, Finset.weightedVSub_const_smul, LinearMap.toMatrix'_mul, groupCohomology.mem_cocycles₂_of_comp_eq_d₁₂, Matrix.proj_comp_diagLinearMap, Submodule.quotientPi_apply, Germ.coe_sum, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, LinearEquiv.coe_curry_symm, groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply, PowerBasis.constr_pow_gen, Matrix.Module.instIsScalarTowerForall, Finset.sum_smul_const_vsub_eq_neg_weightedVSub, ProbabilityTheory.iIndepFun.indepFun_finset_sum_of_notMem, groupCohomology.isoCocycles₁_inv_comp_iCocycles, Projectivization.mk_eq_mk_iff_crossProduct_eq_zero, Matrix.Module.scalar_smul, Matrix.diagonal_toLin', ContinuousAlternatingMap.pi_apply, IsAdjoinRootMonic.ext_elem_iff, Matrix.charpoly_toLin', Lagrange.iterate_derivative_interpolate, Matrix.toLinearMap₂'_toMatrix', LinearEquiv.piCongrLeft'_symm_apply, Matrix.toLinearMapₛₗ₂'_apply, lp.coeFn_sum, LinearEquiv.piCongrRight_symm, Matrix.toLin'_pow, LinearMap.pi_ext_iff, Ideal.ker_tensorProductMk_quotient, Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower_1, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom, Finset.affineCombination_apply, NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst, Matrix.toLinAlgEquiv'_apply, TensorProduct.piRightHom_tmul, groupCohomology.coboundariesOfIsCoboundary₁_coe, Multiset.aestronglyMeasurable_sum, fderivWithin_continuousMultilinearMapCompContinuousLinearMap, ProbabilityTheory.aestronglyMeasurable_exp_mul_sum, Matrix.minpoly_toLin', LinearMap.BilinForm.nondegenerate_toMatrix'_iff, HasMFDerivWithinAt.sum, MultilinearMap.fromDirectSumEquiv_lof, Submodule.closure_coe_iSup_map_single, NumberField.mixedEmbedding.span_latticeBasis, LinearMap.toMatrix'_intrinsicStar, QuadraticMap.pi_apply_single, ProbabilityTheory.Kernel.coe_finset_sum, Algebra.PreSubmersivePresentation.aevalDifferential_single, cross_apply, MeasureTheory.ProgMeasurable.finset_sum', Filter.isBoundedUnder_sum, Nat.isSemilinearSet_setOf_mulVec_eq, IsLocalFrameOn.coeff_apply_of_notMem, NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite, Fintype.range_linearCombination, DFinsupp.lsum_single, LinearMap.toMatrixAlgEquiv'_toLinAlgEquiv', Matrix.represents_iff, MeasureTheory.stoppedValue_sub_eq_sum', LinearMap.pi_proj_comp, Submodule.IsLattice.finrank_of_pi, floorDiv_def, vecMulVecBilin_apply_apply, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, isAdjointPair_toLinearMap₂', Matrix.toLin'_apply', Configuration.ofField.crossProduct_eq_zero_of_dotProduct_eq_zero, Matrix.Represents.congr_fun, Finsupp.coe_finset_sum, ZMod.dft_comp_neg, Rep.coindIso_inv_hom_hom, Matrix.ker_toLin'_eq_bot_iff, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, LinearMap.vecCons₂_apply, Finsupp.lsum_apply, LinearMap.toMatrix'_toLinearMap₂', Finset.weightedVSubOfPoint_smul, groupCohomology.cocycles₁_map_mul_of_isTrivial, contMDiffOn_finset_sum', Polynomial.toFn_comp_ofFn_eq_id, MultilinearMap.dfinsuppFamilyₗ_apply, Submodule.pi_liftQ_eq_liftQ_pi, LinearMap.BilinForm.mul_toMatrix', NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces, MeasureTheory.stoppedProcess_eq'', ValueDistribution.characteristic_sum_top_le, Finsupp.coe_lsum, MeasureTheory.Measure.coe_finset_sum, QuadraticForm.equivalent_sum_squares, Submodule.IsLattice.rank_of_pi, LinearMap.toMatrixRight'_id, leibniz_cross, HVertexOperator.coeff_inj, fwdDiff_aux.fwdDiffₗ_apply, PiToModule.fromEnd_apply_single_one, Finset.weightedVSubOfPoint_vadd_eq_of_sum_eq_one, Rep.indToCoindAux_mul_snd, groupCohomology.cocycles₁IsoOfIsTrivial_inv_hom_apply_coe, Matrix.nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂, MultilinearMap.map_add_eq_map_add_linearDeriv_add, fwdDiff_aux.shiftₗ_apply, MultilinearMap.piFamily_apply, IsAdjoinRootMonic.coeff_apply_lt, LinearEquiv.finTwoArrow_symm_apply, groupCohomology.cocyclesOfIsMulCocycle₂_coe, Finset.indicator_sum, Finsupp.sigmaFinsuppLEquivPiFinsupp_apply, orthonormalBasis.toBasis, IsLocalFrameOn.coeff_apply_zero_at, LinearMap.compLeft_apply, ContDiffMapSupportedIn.isUniformEmbedding_pi_structureMapCLM, ContinuousMultilinearMap.piEquiv_apply, summable, NormedAddGroupHom.coe_sum, MeasureTheory.uniformIntegrable_average, groupCohomology.coboundariesOfIsMulCoboundary₁_coe, DirichletCharacter.IsPrimitive.fourierTransform_eq_inv_mul_gaussSum, convexHull_pi, NumberField.Units.instDiscrete_unitLattice, Finsupp.llift_symm_apply, Matrix.ker_diagonal_toLin', LinearEquiv.sumPiEquivProdPi_symm_apply, Matrix.toBilin'_apply, conjneg_sum, ContinuousLinearMap.norm_single, Matrix.adjugate_def, Matrix.PosDef.toQuadraticForm', groupCohomology.H1π_eq_zero_iff, Matrix.toLin'_one, Matrix.Module.smul_apply, Module.Basis.constr_apply_fintype, Matrix.cramer_submatrix_equiv, groupCohomology.coboundaries₁.val_eq_coe, Matrix.mulVecLin_submatrix, DFinsupp.lsum_symm_apply, ZMod.dft_dft, MultilinearMap.piFamilyₗ_apply, MultilinearMap.fromDirectSumEquiv_apply, mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd, NumberField.mixedEmbedding.negAt_symm, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_apply, Module.finrank_fin_fun, RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff, QuadraticMap.Isometry.proj_apply, ContinuousAlternatingMap.piLIE_symm_apply_apply, IsAdjoinRootMonic.coeff_injective, endVecAlgEquivMatrixEnd_apply_apply, groupCohomology.cocyclesMk₁_eq, Matrix.mulVec_eq_sum, instInvertibleReprₛ, MeromorphicOn.sum, Matrix.trace_toLin'_eq, Finset.weightedVSub_filter_of_ne, NumberField.mixedEmbedding.negAt_apply_isReal_and_mem, Matrix.vecMul_sum, Matrix.toLin'OfInv_symm_apply, QuadraticForm.posDef_of_toMatrix', MultilinearMap.piFamily_single_left_apply, Finset.weightedVSub_vadd, QuadraticAlgebra.linearEquivTuple_symm_apply, hasStrictFDerivAt_list_prod_attach', LinearIndependent.fintypeLinearCombination_injective, NumberField.mixedEmbedding.volume_negAt_plusPart, CircleIntegrable.sum, ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_sum_of_notMem, Module.Basis.parallelepiped_eq_map, TensorProduct.piScalarRight_symm_single, ContinuousAlternatingMap.piLinearEquiv_symm_apply, Module.finrank_pi_fintype, Ideal.constr_basisSpanSingleton, MeasureTheory.stoppedProcess_eq_of_mem_finset, counit_coe_finsupp, Finset.weightedVSubOfPoint_apply_const, Lex.isOrderedAddCancelMonoid, Algebra.TensorProduct.piRightHom_one, LinearMap.pi_comp, Submodule.iSup_map_single, ProbabilityTheory.iIndepFun.hasGaussianLaw, RCLike.linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero, groupCohomology.coboundariesToCocycles₂_apply, linearIndependent_iff_injective_fintypeLinearCombination, Polynomial.injective_ofFn, Module.Basis.coePiBasisFun.toMatrix_eq_transpose, LinearMap.mapMatrixModule_comp, LinearMap.toMatrix'_comp, Matrix.toLinearEquiv'_apply, LinearMap.isUnit_toMatrix'_iff, Submodule.quotientPi_symm_apply, ZLattice.volume_image_eq_volume_div_covolume, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_apply, Real.map_linearMap_volume_pi_eq_smul_volume_pi, Finsupp.bilinearCombination_apply, groupCohomology.cocyclesOfIsMulCocycle₁_coe, groupCohomology.H2π_eq_zero_iff, SlashInvariantForm.coe_trace, DFinsupp.ker_mapRangeLinearMap, Matrix.cramer_subsingleton_apply, Matrix.toBilin'_comp, MeasureTheory.Submartingale.sum_smul_sub', groupCohomology.mapCocycles₁_comp_i_assoc, NumberField.mixedEmbedding.iUnion_negAt_plusPart_union, ContinuousMultilinearMap.norm_iteratedFDeriv_le', hasStrictFDerivAt_finset_prod, groupCohomology.cocycles₁.val_eq_coe, Lagrange.degree_interpolate_le, PiLp.basisFun_eq_pi_basisFun, groupCohomology.H1π_comp_map_apply, LinearMap.proj_pi, Matrix.cramer_is_linear, groupCohomology.cocycles₁_map_one, MeasureTheory.Measure.map_linearMap_addHaar_pi_eq_smul_addHaar, pi_eq_sum_univ, hasFDerivAtFilter_finCons, ContinuousLinearMap.pi_comp, contMDiffWithinAt_finset_sum', NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, groupCohomology.π_comp_H2Iso_hom_assoc, Submodule.quotientPi_aux.map_add, convex_stdSimplex, LSeries_sum, Module.Finite.exists_comp_eq_id_of_projective, MeasureTheory.locallyIntegrable_finset_sum', groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, DFinsupp.coeFnLinearMap_apply, Finset.weightedVSubOfPoint_eq_of_weights_eq, MultilinearMap.piFamily_single_left, LinearMap.toMatrix'_id, weightedVSub_mem_vectorSpan, HasSum.matrix_blockDiag, EuclideanGeometry.inner_weightedVSub, ContinuousMultilinearMap.iteratedFDerivComponent_apply, LinearMap.pi_proj, Projectivization.cross_mk, ValueDistribution.logCounting_sum_top_eventuallyLE, LinearMap.coe_single, ZLattice.covolume.tendsto_card_le_div, LinearMap.nondegenerate_toMatrix₂'_iff, QuadraticMap.weightedSumSquares_apply, LinearMap.BilinForm.toMatrix'_comp, IntervalIntegrable.finsum, ContinuousLinearMap.coe_sum', DFinsupp.lmk_apply, Filter.isBoundedUnder_le_sum, triple_product_eq_det, LinearEquiv.funCongrLeft_id, Matrix.toLinearMap₂_basisFun, MeasureTheory.stoppedValue_sub_eq_sum, NumberField.mixedEmbedding.injective_mixedSpaceOfRealSpace, LinearEquiv.funUnique_apply, LinearEquiv.sumArrowLequivProdArrow_apply_fst, LinearMap.sum_single_apply, Matrix.toLinearMapRight'_apply, ContinuousLinearMap.proj_pi, ContinuousMultilinearMap.piₗᵢ_symm_apply, Finset.weightedVSub_congr, Matrix.instIsScalarTowerForall, QuadraticMap.pi_apply, Subalgebra.pi_toSubsemiring, Continuous.matrix_cramer, cfcₙ_sum, Finsupp.linearEquivFunOnFinite_apply, LinearMap.vecEmpty_apply, Rep.coindVEquiv_apply_hom, Matrix.linearIndependent_rows_of_det_ne_zero, Matrix.Module.single_smul, LinearMap.nondegenerate_toLinearMap₂'_iff_det_ne_zero, Finset.measurable_sum_apply, Matrix.mulVecBilin_apply, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_assoc, SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, LinearMap.pi_ext'_iff, MultilinearMap.piFamily_smul, lieEquivMatrix'_symm_apply, Matrix.proj_diagonal, openSegment_subset, fderiv_continuousMultilinearMapCompContinuousLinearMap, comul_coe_finsupp, NumberField.mixedEmbedding.stdBasis_apply_isReal, Finset.analyticOnNhd_sum, Module.annihilator_pi, IsLocalFrameOn.eq_iff_coeff, ZMod.completedLFunction_one_sub_odd, groupCohomology.cocycles₂.val_eq_coe, Algebra.SubmersivePresentation.cotangentComplexAux_surjective, LinearMap.continuous_on_pi, Matrix.linfty_opNorm_toMatrix, NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, Algebra.TensorProduct.piRight_tmul, MvPolynomial.ker_evalₗ, Matrix.toBilin'_apply', ContinuousMultilinearMap.opNNNorm_pi, Matrix.toLinearMap₂'_single, ExteriorAlgebra.liftAlternating_comp_ιMulti, Matrix.smul_eq_mulVec, FunOnFinite.linearMap_id, LinearMap.separatingRight_toLinearMap₂'_of_det_ne_zero', UniformOnFun.toFun_sum, LinearEquiv.piCurry_symm_apply, Polynomial.eval_eq_sum_degreeLTEquiv, ContinuousMultilinearMap.coe_pi, ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap, IsAdjoinRootMonic.coeff_algebraMap, Module.Basis.equivFun_apply, NumberField.mixedEmbedding.convexBodyLT_convex, HasStrictFDerivAt.sum, FixedPoints.linearIndependent_smul_of_linearIndependent, ContinuousMapZero.coe_sum, ProbabilityTheory.iIndepFun_iff_charFunDual_pi', Lagrange.interpolate_eq_add_interpolate_erase, Matrix.SpecialLinearGroup.toLin'_to_linearMap, groupCohomology.isoCocycles₂_inv_comp_iCocycles, LinearMap.mul_toMatrix₂'_mul, LinearMap.toMatrix₂'_mul, Finset.eq_weightedVSub_subset_iff_eq_weightedVSub_subtype, derivWithin_sum, ZLattice.volume_image_eq_volume_div_covolume', Submodule.fg_iff_exists_fin_linearMap, Finset.weightedVSub_eq_linear_combination, LinearMap.intrinsicStar_single, Matrix.separatingLeft_toLinearMap₂'_iff, groupCohomology.δ₀_apply, Finsupp.linearEquivFunOnFinite_symm_single, triple_product_permutation, LinearMap.separatingLeft_toLinearMap₂'_of_det_ne_zero', Polynomial.ofFn_degree_lt, hasSum, basisFun_apply, Lagrange.interpolate_apply, Submodule.piQuotientLift_single, Lagrange.interpolate_eq_iff_values_eq_on, crossProduct_ne_zero_iff_linearIndependent, ContinuousLinearMap.hasFDerivAt_uncurry_of_multilinear, Matrix.separatingLeft_toBilin'_iff, Subalgebra.coe_pi, circleAverage_log_norm_factorizedRational, groupCohomology.cocyclesMk₂_eq, Module.Basis.toMatrix_eq_toMatrix_constr, Finset.weightedVSub_vadd_affineCombination, Ideal.pi_mkQ_rTensor, HasStrictFDerivAt.continuousMultilinearMapCompContinuousLinearMap, MeasureTheory.stoppedProcess_eq', PiLp.hasFDerivAt_ofLp, Matrix.mulVec_cramer, LinearMap.proj_comp_single, Matrix.cramerMap_is_linear, NumberField.mixedEmbedding.latticeBasis_apply, Matrix.instSMulCommClassForall, Submodule.quotientPi_aux.left_inv, ProbabilityTheory.covariance_sum_left', strongRankCondition_iff_forall_zero_lt_finrank, HasDerivAt.sum, groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply, DFinsupp.linearEquivFunOnFintype_apply, Finset.weightedVSub_apply, Matrix.toBilin'Aux_eq, rank_fin_fun, Finset.weightedVSubOfPoint_eq_of_sum_eq_zero, LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix', groupCohomology.isoCocycles₁_hom_comp_i, MeasureTheory.martingalePart_eq_sum, ProbabilityTheory.mgf_sum_of_identDistrib, LinearMap.toMatrixAlgEquiv'_symm, ZMod.dft_const_mul, QuadraticForm.equivalent_sign_ne_zero_weighted_sum_squared, ContinuousLinearMap.coe_proj, ProbabilityTheory.Kernel.iIndepFun.indepFun_sum_range_succ₀, Finset.weightedVSubOfPoint_const_smul, Matrix.toPerfectPairing, comul_comp_proj, NumberField.mixedEmbedding.commMap_apply_of_isReal, LinearMap.mapMatrixModule_id, groupCohomology.mapCocycles₁_comp_i_apply, LinearEquiv.sumArrowLequivProdArrow_apply_snd, Finset.analyticOn_sum, Rep.coindMap_hom, MeasureTheory.lpNorm_sum_le, instModuleIsTorsionFree, NumberField.mixedEmbedding.hasFDerivAt_polarCoordReal_symm, ContinuousMap.coe_sum, Finset.analyticAt_sum, groupCohomology.cocycles₂_ext_iff, Matrix.toLinearEquivRight'OfInv_apply, MeasureTheory.Submartingale.sum_smul_sub, hasEigenvalue_toLin'_diagonal_iff, ContinuousLinearMapWOT.continuous_inducingFn, LinearMap.toMatrix'_toLinearMapₛₗ₂', DirectSum.coeFnLinearMap_apply, BilinForm.toMatrix_basisFun, MeasureTheory.charFunDual_eq_pi_iff', Matrix.toLin'_submatrix, IsAdjoinRootMonic.coeff_one, stdSimplex.image_linearMap, ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_sum, NumberField.mixedEmbedding.latticeBasis_repr_apply, Affine.Simplex.mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter, cross_dot_cross, LinearMap.ker_compLeft, PiToModule.fromMatrix_apply, Polynomial.surjective_toFn, MeasureTheory.stoppedValue_eq', Lagrange.interpolate_empty, Algebra.SubmersivePresentation.aevalDifferentialEquiv_apply, groupCohomology.cochainsMap_f_hom, LinearEquiv.piFinTwo_apply, Matrix.linfty_opNorm_eq_opNorm, groupCohomology.coboundaries₁_ext_iff, DirectSum.range_lmap, iSupIndep_iff_dfinsupp_lsum_injective, span_flip_eq_top_iff_linearIndependent, Finsupp.linearCombination_eq_fintype_linearCombination, max_aleph0_card_le_rank_fun_nat, NumberField.mixedEmbedding.normAtPlace_negAt, ContinuousLinearMap.norm_pi_le_of_le, Lagrange.eq_interpolate_of_eval_eq, Matrix.cramer_one, Algebra.TensorProduct.equivPiOfFiniteBasis_symm_apply, Finsupp.lsum_comp_lsingle, Matrix.separatingRight_toBilin'_iff, LinearMap.vecEmpty₂_apply, groupCohomology.π_comp_H2Iso_hom_apply, DFinsupp.coe_finset_sum, LinearMap.range_compLeft, Matrix.toLinAlgEquiv'_toMatrixAlgEquiv', NumberField.mixedEmbedding.finrank, isNoetherian_pi, LinearMap.funLeft_apply, Module.Basis.constr_basis, ContinuousMultilinearMap.piEquiv_symm_apply, ValueDistribution.logCounting_sum_top_le, Finset.aestronglyMeasurable_sum, QuaternionAlgebra.coe_linearEquivTuple, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd, Projectivization.cross_mk_of_ne, LinearEquiv.sumArrowLequivProdArrow_symm_apply_inl, LinearMap.single_apply, endVecAlgEquivMatrixEnd_symm_apply_apply, ContinuousLinearMap.norm_single_le_one, Representation.coind_apply, QuadraticMap.Ring.associated_pi, ProbabilityTheory.iIndepFun.hasGaussianLaw_sum, FunOnFinite.linearMap_piSingle, NumberField.mixedEmbedding.negAt_apply_norm_isReal, linearIndependent_single_one, Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower, Matrix.toLinAlgEquiv'_one, hasStrictFDerivAt_list_prod, groupCohomology.π_comp_H1Iso_hom_apply, ProbabilityTheory.strong_law_aux1, VertexOperator.ncoeff_of_coeff, LSeries.term_sum_apply, Lagrange.eval_interpolate_at_node, Meromorphic.sum, ExteriorAlgebra.liftAlternating_algebraMap, VertexOperator.ncoeff_eq_zero_of_lt_order, comul_single, ZMod.invDFT_def, Submodule.le_comap_single_pi, Matrix.toLin_eq_toLin', TensorProduct.equivFinsuppOfBasisRight_symm, Polynomial.ofFn_comp_toFn_eq_id_of_natDegree_lt, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply, NumberField.Units.unitLattice_rank, HVertexOperator.compHahnSeries_coeff, Submodule.coe_pi, Submodule.quotientPiLift_mk, Matrix.Nondegenerate.toBilin', Lagrange.interpolate_poly_eq_self, LinearMap.BilinForm.toMatrix'_mul, dotProductBilin_apply_apply, Matrix.sum_mulVec, MultilinearMap.piFamily_single, Algebra.traceMatrix_of_basis_mulVec, AddMonoidHom.coe_dfinsuppSum, instIsStablyFiniteRingEndForallOfFinite, PiLp.coe_symm_continuousLinearEquiv, LinearMap.toMatrix₂'_compl₂, Matrix.toLinAlgEquiv'_symm, Matrix.instIsScalarTowerMulOppositeForallOfSMulCommClass, IsAdjoinRootMonic.coeff_apply_coe, eqOn_finsetSum, Finset.expect_apply, ZSpan.discreteTopology_pi_basisFun, Matrix.Module.diagonal_const_smul, ContinuousLinearMap.pi_proj_comp, ProbabilityTheory.strong_law_aux2, Matrix.nondegenerate_toLinearMap₂'_iff, Module.pi_induction, Matrix.SpecialLinearGroup.toLin'_injective, QuadraticMap.coeFn_sum, TensorProduct.piScalarRight_apply, NumberField.Units.logEmbeddingEquiv_apply, Matrix.mulVecLin_reindex, LinearMap.iSup_range_single_le_iInf_ker_proj, LocallyConstant.coeFnₗ_apply, image_update_segment, Finset.sum_smul_vsub_const_eq_weightedVSub, Matrix.cramer_smul, ProbabilityTheory.IndepFun.variance_sum, Matrix.UnitaryGroup.toLin'_mul, LSeriesHasSum.sum, LinearMap.disjoint_single_single, IsLocalFrameOn.coeff_eq_of_eq, AddChar.linearIndependent, LinearMap.pi_zero, isArtinian_pi, HVertexOperator.coeff_comp, Submodule.quotientPi_aux.right_inv, Function.ExtendByZero.linearMap_apply, Finset.sum_fn, ProbabilityTheory.strong_law_aux3, Filter.isBoundedUnder_ge_sum, jacobi_cross, HVertexOperator.coeff_apply_apply, Module.Finite.pi, Set.Finite.convexHull_eq_image, AdicCompletion.piEquivOfFintype_apply, ProbabilityTheory.iIndepFun.indepFun_finset_sum_of_notMem₀, HasMFDerivAt.sum, Rep.indToCoindAux_snd_mul_inv, tendsto_card_div_pow_atTop_volume', MeasureTheory.charFunDual_pi, DirectSum.linearEquivFunOnFintype_symm_single, LinearMap.BilinForm.toMatrix'_toBilin', Fintype.linearCombination_apply_single, SimplexCategory.coe_toTopMap, Fintype.linearCombination_apply, neg_cross, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom, ProbabilityTheory.covariance_sum_sum', PowerBasis.liftEquiv'_symm_apply_apply, ProbabilityTheory.variance_sum', comul_coe_dFinsupp, MultilinearMap.linearDeriv_apply, PowerBasis.constr_pow_mul, QuadraticMap.nonneg_pi_iff, LinearMap.det_toMatrix', ENNReal.tsum_apply, convexHull_rangle_single_eq_stdSimplex, Matrix.mulVec_injective_iff, MeasureTheory.lpNorm_expect_le, groupCohomology.coboundaries₁_le_cocycles₁, Module.Finite.exists_fin', segment_subset, Matrix.toLin'OfInv_apply, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_expMap_symm, Basis.equivFun_symm_single, NumberField.mixedEmbedding.measurableSet_negAt_plusPart, UniformFun.ofFun_sum, Module.finrank_fintype_fun_eq_card, Finset.analyticWithinAt_sum, MultilinearMap.pi_ext_iff, rank_fun, UniformFun.toFun_sum, Module.Basis.constr_self, Matrix.UnitaryGroup.toGL_one, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, NumberField.mixedEmbedding.convexBodySum_convex, Finset.weightedVSub_subtype_eq_filter, Matrix.SeparatingRight.toBilin', IsAdjoinRootMonic.coeff_apply_le, ContinuousMultilinearMap.piₗᵢ_apply, LinearMap.ltoFun_apply, Module.Basis.opNNNorm_le, groupCohomology.isoCocycles₂_hom_comp_i_apply, Rep.diagonalHomEquiv_apply, Matrix.range_diagonal, ZMod.completedLFunction_one_sub_even, hasStrictFDerivAt_list_prod', MeasureTheory.integrable_finset_sum', Matrix.piLinearEquiv_symm_apply, Matrix.diag_sum, Finset.sum_smul_const_vsub_eq_sub_weightedVSubOfPoint, LinearMap.proj_surjective, Module.Basis.constr_def, rank_fun', Rep.freeLiftLEquiv_symm_apply, Finsupp.coe_sum, AddChar.coe_complexBasis, LinearMap.toMatrix₂'_comp, groupCohomology.coboundaries₂_ext_iff, Polynomial.ofFn_coeff_eq_val_of_lt, Finset.weightedVSubOfPoint_erase, IsAdjoinRootMonic.coeff_root, Matrix.coe_ofLinearEquiv_symm, floorDiv_apply, Rep.indToCoindAux_of_not_rel, groupCohomology.cocyclesOfIsCocycle₂_coe, LinearMap.toMatrix_eq_toMatrix', Matrix.diagonal_tsum, fwdDiff_aux.coe_fwdDiffₗ_pow, Matrix.SpecialLinearGroup.toLin'_symm_apply, Finset.weightedVSub_sdiff_sub, PiLp.hasStrictFDerivAt_ofLp, ContinuousMultilinearMap.fderivCompContinuousLinearMap_apply, groupCohomology.H1π_comp_map, basisFun_equivFun, LinearMap.toMatrix'_one, NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace, NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm, rank_fun_eq_lift_mul, Module.Basis.opNorm_le, Module.surjective_piEquiv_apply_iff, AlternatingMap.pi_apply, ContinuousAlternatingMap.opNorm_pi, NumberField.mixedEmbedding.fundamentalCone.expMap_sum, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, cross_cross_eq_smul_sub_smul', LinearMap.toMatrixₛₗ₂'_apply, starConvex_pi, Submodule.mem_biSup_iff_exists_dfinsupp, Module.Basis.coe_ofEquivFun, Matrix.toLinearMapRight'_one, PiLp.continuousLinearEquiv_apply, Matrix.maxGenEigenspace_toLin'_diagonal_eq_eigenspace, DirichletCharacter.fourierTransform_eq_gaussSum_mulShift, MultilinearMap.pi_apply, Matrix.cramer_transpose_apply, Finset.sum_smul_vsub_const_eq_weightedVSubOfPoint_sub, NumberField.mixedEmbedding.disjoint_span_commMap_ker, deriv_sum, Finset.weightedVSub_indicator_subset, LinearEquiv.piCongrRight_refl, ContinuousLinearMap.coe_pi', Module.Basis.sum_equivFun, counit_comp_single, SymmetricAlgebra.IsSymmetricAlgebra.mvPolynomial, Module.Finite.exists_fin_quot_equiv, TensorProduct.piScalarRightHom_tmul, Submodule.topologicalClosure_iSup_map_single, LinearMap.lsum_piSingle, Algebra.TensorProduct.equivPiOfFiniteBasis_apply, ModularForm.coe_trace, IsLocalFrameOn.coeff_sum_eq, Module.Basis.constr_range, TensorProduct.piRight_apply, ZMod.dft_eq_fourier, Algebra.TensorProduct.piScalarRight_tmul_apply, ZMod.dft_odd_iff, Matrix.toLin'_apply, ContinuousLinearMap.pi_zero, AddChar.complexBasis_apply, ceilDiv_apply, LinearMap.proj_comp_single_ne, Fintype.sum_apply, Module.Basis.constr_apply, Matrix.blockDiagonal'_tsum, LinearEquiv.piCongrLeft'_apply, mem_span_range_single_inl_iff, DFinsupp.lsum_apply_apply, MeasureTheory.stoppedValue_eq_of_mem_finset, Polynomial.degreeLTEquiv_eq_zero_iff_eq_zero, Finsupp.linearCombination_eq_fintype_linearCombination_apply, isOrderedAddMonoid, ValueDistribution.characteristic_sum_top_eventuallyLE, LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero, Matrix.Module.smul_def', QuadraticMap.Equivalent.pi, Finset.weightedVSubOfPoint_subtype_eq_filter, QuadraticMap.IsometryEquiv.pi_toLinearEquiv, weightedVSub_mem_vectorSpan_pair, QuadraticMap.Ring.polar_pi, MultilinearMap.piFamily_compLinearMap_lsingle, strongRankCondition_iff_succ, Matrix.toEuclideanLin_toLp, instIsCocomm, groupCohomology.cocycles₁_ext_iff, PowerBasis.constr_pow_aeval, LinearMap.CompatibleSMul.pi, IsBaseChange.finitePow, LinearMap.ker_single, ProbabilityTheory.iIndepFun.cgf_sum₀, Matrix.linearIndependent_cols_of_invertible, Matrix.toLin'_toMatrix', LinearEquiv.funCongrLeft_comp, iteratedDeriv_sum, Matrix.coe_ofLinearEquiv, Submodule.iInf_comap_proj, ZMod.LFunction_dft, LinearMap.BilinForm.nondegenerate_toBilin'_of_det_ne_zero', basisFun_repr, Polynomial.ofFn_coeff_eq_zero_of_ge, Module.Basis.toDual_eq_equivFun, ZMod.dft_const_smul, fwdDiff_aux.coe_fwdDiffₗ, LinearMap.toMatrix₂'_apply, Matrix.vecMul_injective_iff, contMDiffAt_finset_sum', NumberField.mixedEmbedding.fundamentalCone.linearIndependent_completeFamily, fderivWithin_sum, NumberField.mixedEmbedding.commMap_canonical_eq_mixed, Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, hasFDerivAtFilter_pi', TensorProduct.sum_tmul_basis_left_injective, ZMod.dft_smul_const, NumberField.mixedEmbedding.norm_negAt, Matrix.mulVec_one, Real.volume_preserving_transvectionStruct, ContinuousAlternatingMap.piLinearEquiv_apply, Matrix.toBilin'_toMatrix', contMDiff_finset_sum', groupCohomology.isoCocycles₂_hom_comp_i_assoc, Matrix.rank_eq_finrank_span_cols, LinearMap.toMatrix'_mulVec, Module.Finite.pi_iff, CircleIntegrable.finsum, VertexOperator.coeff_eq_ncoeff, LinearMap.lsum_symm_apply, HasDerivWithinAt.sum, MeasureTheory.eLpNorm_sum_le, Rep.coindIso_hom_hom_hom, LinearMap.separatingRight_toLinearMap₂'_iff_det_ne_zero, Module.Basis.coord_equivFun_symm, ZMod.dft_def, dotProduct_toMatrix₂_mulVec, hasFDerivAt_pi', Matrix.entryLinearMap_eq_comp, ContinuousMultilinearMap.hasStrictFDerivAt_uncurry, Matrix.diagonal_comp_single, rank_pi, Measurable.ennreal_tsum', groupCohomology.coe_mapCocycles₂, DifferentiableAt.sum, LinearRecurrence.is_sol_iff_mem_solSpace, AdicCompletion.piEquivFin_apply, Fin.consEquivL_symm_apply, LinearMap.const_apply, QuadraticMap.basisRepr_apply, isNoetherian_pi', hasFDerivAt_list_prod_attach', Finset.aemeasurable_sum, MeasureTheory.setToFun_finset_sum', groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_assoc, MultilinearMap.fromDFinsuppEquiv_symm_apply, groupCohomology.H1π_eq_iff, ContinuousLinearEquiv.piCongrRight_symm_apply, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace, LinearMap.BilinForm.toMatrix'_compRight, groupCohomology.isoCocycles₁_hom_comp_i_assoc, VertexOperator.coeff_eq_zero_of_lt_order, AnalyticOnNhd.eval_continuousLinearMap, Matrix.op_smul_eq_vecMul, Module.FinitePresentation.pi, counit_single, ExteriorAlgebra.liftAlternating_ι, Module.Free.function, ContinuousLinearEquiv.coe_funUnique_symm, Polynomial.ofFn_natDegree_lt, Matrix.rank_vecMulVec, ContinuousLinearEquiv.piCongrRight_apply, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, MvPolynomial.range_evalᵢ, TannakaDuality.FiniteGroup.rightRegular_apply, groupCohomology.coboundariesOfIsCoboundary₂_coe, ProbabilityTheory.iIndepFun.mgf_sum, NumberField.mixedEmbedding.disjoint_negAt_plusPart, Algebra.SubmersivePresentation.cotangentEquiv_apply, ContinuousLinearEquiv.piFinTwo_symm_apply, LinearMap.toMatrixRight'_comp, CompactlySupportedContinuousMap.coe_sum, ProbabilityTheory.iCondIndepFun.condIndepFun_sum_range_succ, Module.Basis.constr_eq, Fin.consLinearEquiv_symm_apply, QuadraticMap.toMatrix'_smul, HVertexOperator.coeff_of_coeff, summable_matrix_blockDiagonal, Algebra.SubmersivePresentation.basisDeriv_apply, Lagrange.interpolate_singleton, SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj, isArtinian_pi', DirectSum.linearEquivFunOnFintype_symm_coe, SimpleGraph.mem_ker_toLin'_lapMatrix_of_connectedComponent, lsum_comp_mapRange_toSpanSingleton, AddMonoidHom.coe_finsuppSum, DirectSum.linearEquivFunOnFintype_apply, groupCohomology.mapCocycles₁_comp_i, MeasureTheory.StronglyMeasurable.Finset.stronglyMeasurable_sum_apply, Matrix.SpecialLinearGroup.toLin'_apply, ContinuousLinearEquiv.coe_funUnique, Matrix.GeneralLinearGroup.toLin_apply, Matrix.mulVecLin_mul, DifferentiableOn.sum, Submodule.piQuotientLift_mk, MvPolynomial.evalₗ_apply, ProbabilityTheory.variance_sum, LinearMap.mapMatrixModule_comp_apply, comul_comp_finsuppLcoeFun, Multiset.measurable_sum, Matrix.linearIndependent_rows_iff_isUnit, NumberField.mixedEmbedding.convexBodyLT'_convex, groupCohomology.cocycles₁.d₁₂_apply, orderedSMul, HasFDerivWithinAt.sum, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, Int.submodule_toAddSubgroup_index_ne_zero_iff, Matrix.Nondegenerate.toLinearMap₂', groupCohomology.π_comp_H2Iso_hom, Finset.sum_smul_vsub_eq_weightedVSub_sub, Finset.weightedVSubOfPoint_sdiff_sub, Matrix.separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂, Finsupp.lsum_symm_apply, IsAdjoinRootMonic.coeff_root_pow, NumberField.mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, ZMod.dft_apply_zero, LinearMap.toMatrixAlgEquiv'_comp, BoxIntegral.unitPartition.tag_mem_smul_span, NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces, ContMDiffMap.coeFnLinearMap_apply, Matrix.cramer_eq_adjugate_mulVec, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, MDifferentiableWithinAt.sum, LieModule.toEnd_matrix, Matrix.det_smul_inv_vecMul_eq_cramer_transpose, ContinuousLinearEquiv.piFinTwo_apply, ZLattice.covolume_eq_det, Fin.consLinearEquiv_apply, LinearMap.proj_comp_single_same, LinearMap.toLinearMap₂'Aux_toMatrix₂Aux, QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate', Matrix.toBilin'_single, LinearEquiv.funCongrLeft_symm, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply, LinearEquiv.piRing_apply, PiLp.hasStrictFDerivAt_toLp, Matrix.spectrum_toLin', hasFDerivAt_finset_prod, MultilinearMap.piFamily_zero
addCommSemigroup 📖	CompOp	—
addGroup 📖	CompOp	66 math math: NumberField.mixedEmbedding.fundamentalDomain_integerLattice, DFinsupp.range_mapRangeAddMonoidHom, AddSubgroup.mem_pi, AddSubgroup.pi_top, AddMonoidHom.noncommPiCoprod_range, AddSubgroup.pi_bot, BoxIntegral.unitPartition.mem_smul_span_iff, abs_def, negPart_apply, NumberField.mixedEmbedding.instIsAddHaarMeasureMixedSpaceVolume, abs_apply, AddSubgroup.noncommPiCoprod_range, BoundedContinuousFunction.coe_posPart, AddSubgroup.single_mem_pi, NumberField.Units.span_basisOfIsMaxRank, ConvexOn.isBoundedUnder_abs, ProfiniteAddGrp.limit_zero_val, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, AddSubgroup.pi_empty, AddSubgroup.index_pi, Int.addSubgroup_index_ne_zero_iff, Filter.Tendsto.vsub, vsub_apply, NumberField.Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion, QuotientAddGroup.rightRel_pi, MeasureTheory.Submartingale.pos, AddSubgroup.pi_le_iff, RCLike.abs_wInner_le, vsub_def, AddSubgroup.pi_eq_bot_iff, MeasureTheory.Measure.instIsAddHaarMeasureForallVolumeOfMeasurableAddOfSigmaFinite, MeasureTheory.lpNorm_abs, DFinsupp.ker_mapRangeAddMonoidHom, ProfiniteAddGrp.limit_add_val, DirectSum.ker_map, DirectSum.range_map, ProfiniteAddGrp.limit_ext_iff, LipschitzWith.vsub, BoundedContinuousFunction.coe_abs, AddSubgroup.FG.pi, MeasureTheory.addHaarMeasure_eq_volume_pi, Real.abs_circleAverage_le_circleAverage_abs, ConcaveOn.isBoundedUnder_abs, negPart_def, AddSubgroup.le_pi_iff, topologicalAddGroup, AddSubgroup.coe_pi, MeasureTheory.isAddHaarMeasure_volume_pi, posPart_def, posPart_apply, BoundedContinuousFunction.coe_negPart, MeasureTheory.Measure.pi.isAddHaarMeasure, AddSubgroup.closure_pi, NumberField.mixedEmbedding.instIsAddHaarMeasureRealMixedSpaceVolume, CircleIntegrable.abs, instIsUniformAddGroup, ProfiniteAddGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemAddSubgroupLimitConePtAux, instAddGroupFG, QuotientAddGroup.leftRel_pi, HasCompactSupport.abs, AddSubgroup.fg_iff_exists_fin_addMonoidHom, ContinuousMap.coe_abs, BoxIntegral.unitPartition.tag_mem_smul_span, Function.locallyFinsuppWithin.memAddSubgroup, instIsTopologicalAddTorsorForall, MeasureTheory.MemLp.abs
addLeftCancelMonoid 📖	CompOp	—
addLeftCancelSemigroup 📖	CompOp	—
addMonoid 📖	CompOp	126 math math: Finset.map_nsmul_piAntidiag_univ, MemHolder.nsmul, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, ModularForm.mul_slash_SL2, ModularForm.smul_slash, ProbabilityTheory.Kernel.coe_nsmul, AddMonoid.exponent_pi_eq_zero, SlashInvariantForm.slash_action_eq', ModularForm.mul_slash, ChevalleyThm.MvPolynomialC.degBound_casesOn_succ, RootPairing.two_nsmul_reflection_eq_of_perm_eq, OnePoint.isBoundedAt_iff_exists_SL2Z, SlashInvariantForm.quotientFunc_mk, ModularForm.SL_slash, AddSubmonoid.FG.pi, addOrderOf, ModularForm.prod_slash, threeAPFree_pi, ValueDistribution.logCounting_pow_top, AddEquiv.val_neg_piAddUnits_apply, ValueDistribution.proximity_pow_zero, ModularForm.prod_slash_sum_weights, OnePoint.isBoundedAt_iff_forall_SL2Z, SlashInvariantForm.quotientFunc_smul, OnePoint.isZeroAt_iff_exists_SL2Z, LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, addOrderOf_eq_sInf, EisensteinSeries.E2_slash_action, Finset.map_nsmul_piAntidiag, EisensteinSeries.G2_slash_action, BoundedContinuousFunction.coe_nsmulRec, ContMDiffSection.coe_nsmul, SlashInvariantForm.coe_translate, Matrix.instSMulCommClassForall_1, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, Finset.noncommSum_single, Matrix.Module.smul_def, NormedAddGroupHom.coe_nsmul, isAddUnit_iff, birkhoffSum_of_comp_eq, EisensteinSeries.D2_inv, AddMonoid.exponent_pi, OnePoint.isZeroAt_iff_forall_SL2Z, OnePoint.isBoundedAt_iff, OnePoint.IsZeroAt.smul_iff, MDifferentiable.slash, CuspForm.coe_translate, LieModule.trace_comp_toEnd_genWeightSpace_eq, Matrix.Module.instIsScalarTowerForall, Matrix.Module.scalar_smul, EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF, ValueDistribution.characteristic_pow_zero, Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower_1, ModularForm.slash_action_eq'_iff, MeasureTheory.lpNorm_nsmul, instSubsingletonAddUnits, LieAlgebra.toEnd_pow_apply_mem, UpperHalfPlane.petersson_slash_SL, ModularForm.SL_slash_def, LieModule.exists_genWeightSpace_smul_add_eq_bot, eHolderNorm_nsmul, Matrix.Module.smul_apply, OnePoint.IsBoundedAt.smul_iff, Finsupp.coe_nsmul, LieModule.chainTopCoeff_add_one, ValueDistribution.characteristic_pow_top, Finset.noncommSum_add_single, Function.locallyFinsuppWithin.coe_nsmul, MemHolder.nnHolderNorm_nsmul, Matrix.instIsScalarTowerForall, Matrix.Module.single_smul, LieModule.eventually_genWeightSpace_smul_add_eq_bot, Matrix.smul_eq_mulVec, AddEquiv.val_piAddUnits_symm_apply, LieModuleHom.coe_nsmul, Matrix.instSMulCommClassForall, SlashInvariantForm.slash_S_apply, Complex.ofReal_comp_nsmul, ValueDistribution.proximity_pow_top, ValueDistribution.logCounting_pow_zero, ModularForm.prod_fintype_slash, IsOfFinAddOrder.pi, Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower, ModularFormClass.bdd_at_infty_slash, ModularForm.slash_def, CuspFormClass.zero_at_infty_slash, ModularForm.is_invariant_one', Matrix.instIsScalarTowerMulOppositeForallOfSMulCommClass, Matrix.Module.diagonal_const_smul, LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add, AddEquiv.val_neg_piAddUnits_symm_apply, LieAlgebra.IsKilling.rootSpace_two_smul, ModularForm.is_invariant_const, ModularForm.SL_slash_apply, UpperHalfPlane.IsZeroAtImInfty.slash, ModularForm.coe_translate, EisensteinSeries.eisensteinSeries_slash_apply, HahnSeries.coeff_nsmul, Matrix.Module.smul_def', Representation.IntertwiningMap.coe_nsmul, OnePoint.isZeroAt_iff, LieModule.coe_chainTop', DFinsupp.coe_nsmul, ChevalleyThm.MvPolynomialC.numBound_casesOn_succ, SlashInvariantFormClass.slash_action_eq, SlashInvariantForm.slash_action_eqn, CentroidHom.coe_natCast, instIsAddTorsionFree, AddEquiv.val_piAddUnits_apply, ModularForm.is_invariant_one, instAddMonoidFG, Matrix.op_smul_eq_vecMul, Behrend.threeAPFree_sphere, EisensteinSeries.D2_mul, UpperHalfPlane.IsBoundedAtImInfty.slash, fderiv_norm_sq, ModularForm.SL_smul_slash, EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF, MeasureTheory.eLpNorm_nsmul, Finset.nsmul_piAntidiag_univ, ModularForm.slash_apply, EisensteinSeries.gammaSet_eq_gcd_mul_divIntMap, EisensteinSeries.G2_T_transform, Finset.nsmul_piAntidiag, addOrderOf_apply_dvd_addOrderOf, UpperHalfPlane.petersson_slash
addRightCancelMonoid 📖	CompOp	—
addRightCancelSemigroup 📖	CompOp	—
addSemigroup 📖	CompOp	—
addZeroClass 📖	CompOp	173 math math: ValueDistribution.logCounting_zero, DirectSum.mker_map, MeasureTheory.VectorMeasure.coeFnAddMonoidHom_apply, NumberField.Units.logEmbedding_fundSystem, prevD_comp_left, DirectSum.mrange_map, AddMonoidHom.noncommPiCoprod_apply, AddSubgroup.noncommPiCoprod_single, lp.coeFnAddMonoidHom_apply, AddSubmonoid.iSup_map_single, Matrix.diagLinearMap_apply, Matrix.diagonalLinearMap_apply, AddSubmonoid.pi_le_iff, ProbabilityTheory.Kernel.coeAddHom_apply, MvPolynomial.supDegree_esymmAlgHomMonomial, Function.locallyFinsuppWithin.logCounting_nonneg, DFinsupp.coeFnAddMonoidHom_apply, DirectSum.mk_smul, Behrend.map_mod, Finsupp.coeFnAddHom_apply, Behrend.map_succ, AddMonoidHom.comp_noncommPiCoprod, DirectSum.mk_injective, Behrend.map_le_of_mem_box, Homotopy.prevD_succ_cochainComplex, Function.locallyFinsuppWithin.logCounting_eval_zero, CuspForm.coeHom_apply, ValueDistribution.logCounting_top, LinearMap.BilinForm.coeFnAddMonoidHom_apply, AddSubmonoid.closure_pi, AddSubmonoid.single_mem_pi, ContinuousMap.coeFnAddMonoidHom_apply, AddMonoidHom.coe_dfinsuppSumAddHom, Function.locallyFinsuppWithin.logCounting_eventually_le, AddCommMonCat.coyonedaType_obj_map, AddSubgroup.noncommPiCoprod_apply, Matrix.instSMulCommClassForall_1, AddCommMonCat.coyonedaType_map_app, Finsupp.coe_pointwise_smul, Matrix.entryAddMonoidHom_eq_comp, NumberField.Units.logEmbeddingQuot_apply, NumberField.Units.basisOfIsMaxRank_apply, MeasureTheory.Measure.coeAddHom_apply, AddSubmonoid.pi_eq_bot_iff, prevD_eq_toPrev_dTo, LocallyConstant.coeFnAddMonoidHom_apply, FreeAbelianGroup.liftAddGroupHom_apply, Homotopy.dNext_zero_chainComplex, Fin.accumulate_invAccumulate, Homotopy.prevD_chainComplex, Behrend.map_injOn, Behrend.map_apply, Function.locallyFinsuppWithin.logCounting_eventuallyLE, AddSubmonoid.pi_bot, prevD_nat, AddSubmonoid.le_comap_single_pi, Fin.accumulate_rec, AddSubmonoid.iSup_map_single_le, Matrix.Module.smul_def, AddMonoidHom.single_apply, Derivation.coeFnAddMonoidHom_apply, NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component, DirectSum.mk_apply_of_notMem, ContinuousMap.coeFnLinearMap_apply, Fin.accumulate_apply, SchwartzMap.coeHom_injective, AddSubgroup.injective_noncommPiCoprod_of_iSupIndep, prevD_eq, AddSubmonoid.le_pi_iff, constAddMonoidHom_apply, prevD_eq_zero, DFinsupp.mker_mapRangeAddMonoidHom, MvPolynomial.supDegree_esymm, NumberField.mixedEmbedding.logMap_eq_logEmbedding, AddSubmonoid.pi_empty, AddSubmonoid.fg_iff_exists_fin_addMonoidHom, QuadraticMap.coeFnAddMonoidHom_apply, AddMonoidHom.addCommute_noncommPiCoprod, LieDerivation.coeFnAddMonoidHom_apply, DirectSum.mk_apply_of_mem, Behrend.map_succ', BoundedContinuousFunction.coeFnAddMonoidHom_apply, Matrix.evalAddMonoidHom_comp_diagAddMonoidHom, Matrix.Module.instIsScalarTowerForall, Matrix.Module.scalar_smul, Filter.Germ.coe_coeAddHom, Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower_1, ModularForm.coeHom_apply, ValueDistribution.characteristic_sub_characteristic_inv, AddMonoidHom.noncommPiCoprod_mrange, Matrix.diagonalAddMonoidHom_apply, NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff, AddCommGrpCat.coyonedaType_obj_map, DFinsupp.mrange_mapRangeAddMonoidHom, Matrix.diagAddMonoidHom_apply, dNext_comp_left, ContMDiffSection.coeAddHom_apply, Matrix.blockDiagonal'AddMonoidHom_apply, MeasureTheory.OuterMeasure.coeFnAddMonoidHom_apply, Matrix.Module.smul_apply, locallyFinsuppWithin.logCounting_divisor, Homotopy.dNext_succ_chainComplex, Matrix.blockDiag'AddMonoidHom_apply, NumberField.mixedEmbedding.logMap_unit_smul, Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const, ContMDiffMap.coeFnAddMonoidHom_apply, Matrix.instIsScalarTowerForall, Matrix.Module.single_smul, AddSubmonoid.coe_pi, Matrix.smul_eq_mulVec, DirectSum.coeFnAddMonoidHom_apply, MvPolynomial.weightedDecomposition.decompose'_eq, SchwartzMap.coe_coeHom, NumberField.Units.dirichletUnitTheorem.logEmbedding_component, evalAddMonoidHom_apply, NumberField.Units.logEmbeddingQuot_injective, Matrix.instSMulCommClassForall, dNext_eq_dFrom_fromNext, Function.locallyFinsuppWithin.logCounting_mono, Function.ExtendByZero.hom_apply, Homotopy.prevD_zero_cochainComplex, AddSubmonoid.pi_top, Homotopy.comm, AddMonoidHom.coe_single, dNext_eq, Behrend.map_zero, NormedAddGroupHom.coeAddHom_apply, Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower, AddMonoidHom.coeFn_apply, Function.locallyFinsuppWithin.logCounting_le, ContDiffMapSupportedIn.coe_coeHom, Matrix.blockDiagAddMonoidHom_apply, Seminorm.coeFnAddMonoidHom_apply, Matrix.instIsScalarTowerMulOppositeForallOfSMulCommClass, Matrix.Module.diagonal_const_smul, NumberField.Units.logEmbeddingEquiv_apply, prevD_comp_right, Behrend.map_eq_iff, AddMonoidHom.functions_ext'_iff, AddSubmonoid.mem_pi, Behrend.threeAPFree_image_sphere, Homotopy.dNext_cochainComplex, dNext_comp_right, AddMonoidHom.noncommPiCoprod_single, Matrix.blockDiagonalAddMonoidHom_apply, AddMonoidHom.compLeft_apply, NumberField.Units.regulator_eq_det', SlashInvariantForm.coeHom_injective, ValueDistribution.logCounting_coe, Matrix.Module.smul_def', addMonoidHom_apply, dNext_nat, ValueDistribution.log_counting_zero_sub_logCounting_top, TestFunction.coeFnAddMonoidHom_apply, addMonoidHom_injective, NumberField.Units.dirichletUnitTheorem.logEmbedding_ker, Matrix.mulVec.addMonoidHomLeft_apply, AddMonoidHom.injective_noncommPiCoprod_of_iSupIndep, dNext_eq_zero, Seminorm.coeFnAddMonoidHom_injective, NumberField.Units.regOfFamily_eq_det', ContDiffMapSupportedIn.coeHom_injective, Function.locallyFinsuppWithin.logCounting_even, Matrix.op_smul_eq_vecMul, LeftInvariantDerivation.coeFnAddMonoidHom_apply, ContinuousMapZero.coeFnAddMonoidHom_apply, AddCommGrpCat.coyonedaType_map_app, Fin.accumulate_injective, Fin.accumulate_last, MvPolynomial.decomposition.decompose'_eq, Behrend.map_monotone, MultilinearMap.coeAddMonoidHom_apply, isLinearSet_iff_exists_fin_addMonoidHom
cancelCommMonoid 📖	CompOp	—
cancelMonoid 📖	CompOp	—
commGroup 📖	CompOp	2 math math: CommGrpCat.coyonedaType_map_app, CommGrpCat.coyonedaType_obj_map
commMonoid 📖	CompOp	123 math math: contDiffAt_prod', Finset.univ_prod_mulSingle, ProbabilityTheory.iCondIndepFun.condIndepFun_prod_range_succ, SlashInvariantForm.coe_prodEqualWeights, Finset.analyticOnNhd_prod, Function.FactorizedRational.divisor, MDifferentiableAt.prod, Finset.mulIndicator_prod, hasProd, contMDiff_finset_prod', Finset.stronglyMeasurable_prod, ProbabilityTheory.iIndepFun.indepFun_finset_prod_of_notMem₀, ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_range_succ₀, isOrderedCancelMonoid, ModularForm.prod_slash, MeasureTheory.MemLp.prod, UpperHalfPlane.prod_eq_zero_iff, translate_prod_right, ModularForm.prod_slash_sum_weights, Finset.periodic_prod, MeasureTheory.ProgMeasurable.finset_prod', CommMonCat.coyonedaType_obj_map, Finset.prod_apply, Meromorphic.prod, ProbabilityTheory.iCondIndep_iff, ProbabilityTheory.iCondIndepFun_iff_condExp_inter_preimage_eq_mul, MeromorphicOn.prod, prod_indicator_apply, PiTensorProduct.tprod_prod, ProbabilityTheory.iIndepFun.indepFun_prod_range_succ₀, Germ.coe_prod, contDiffOn_prod', Multiset.aemeasurable_prod, ModularForm.coe_prodEqualWeights, contDiffWithinAt_prod', Function.FactorizedRational.meromorphicOrderAt_eq, eventuallyEq_prod, multiset_prod_apply, Multiset.measurable_prod, Function.FactorizedRational.finprod_eq_fun, Finset.analyticWithinAt_prod, isOrderedMonoid, Finset.aemeasurable_prod, Localization.mapPiEvalRingHom_bijective, ProbabilityTheory.iCondIndepSets_singleton_iff, MDifferentiableOn.prod, contMDiffOn_finset_prod', conjneg_prod, Function.FactorizedRational.meromorphicNFOn_univ, MonoidHom.coe_finsuppProd, Multiset.periodic_prod, UniformFun.toFun_prod, Function.FactorizedRational.analyticAt, ProbabilityTheory.iCondIndepSet_iff, ProbabilityTheory.iIndepFun.indepFun_prod_range_succ, SlashInvariantForm.coe_prod, DifferentiableWithinAt.finset_prod, Finset.aestronglyMeasurable_prod, SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq, Submonoid.IsLocalizationMap.pi, ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_range_succ, MeromorphicAt.prod, DifferentiableOn.finset_prod, UniformFun.ofFun_prod, ProbabilityTheory.iCondIndepSets_iff, Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational, Function.FactorizedRational.log_norm_meromorphicTrailingCoeffAt, Fintype.prod_apply, contDiff_prod', UniformOnFun.ofFun_prod, ProbabilityTheory.iIndepFun.integral_prod_eq_prod_integral, Finset.analyticAt_prod, eqOn_finsetProd, HasDerivWithinAt.finset_prod, ModularForm.coe_prod, HasMFDerivAt.prod, ProbabilityTheory.iCondIndepFun_iff, ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_notMem₀, MonoidHom.coe_dfinsuppProd, deriv_finset_prod, meromorphicTrailingCoeffAt_prod, prod_indicator, MeromorphicOn.extract_zeros_poles, AddChar.coe_prod, prod_indicator_const, Finset.measurable_prod_apply, ModularForm.coe_norm, Function.FactorizedRational.extractFactor, MeasureTheory.StronglyMeasurable.Finset.stronglyMeasurable_prod_apply, Lex.isOrderedCancelMonoid, ModularForm.prod_fintype_slash, finprod_apply, analyticAt_finprod, derivWithin_finset_prod, ContinuousMap.coe_prod, DifferentiableAt.finset_prod, HasStrictDerivAt.finset_prod, ProbabilityTheory.iCondIndepFun.condIndepFun_finset_prod_of_notMem, Differentiable.finset_prod, ProbabilityTheory.iIndepFun.integral_prod_comp, HasDerivAt.finset_prod, Multiset.aestronglyMeasurable_prod, NumberField.mixedEmbedding.fundamentalCone.expMap_sum, Multiset.stronglyMeasurable_prod, contMDiffAt_finset_prod', MonoidHom.coe_finset_prod, UniformOnFun.toFun_prod, HasMFDerivWithinAt.prod, Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational_off_support, BoundedContinuousFunction.coe_prod, Finset.prod_fn, contMDiffWithinAt_finset_prod', MDifferentiable.prod, Filter.BoundedAtFilter.prod, ProbabilityTheory.iIndepFun.indepFun_finset_prod_of_notMem, SlashInvariantForm.coe_norm, CommMonCat.coyonedaType_map_app, Function.FactorizedRational.meromorphicNFOn, MDifferentiableWithinAt.prod, Finset.analyticOn_prod, multipliable, ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_notMem, AddChar.coe_sum
commSemigroup 📖	CompOp	—
divInvMonoid 📖	CompOp	—
divInvOneMonoid 📖	CompOp	—
divisionCommMonoid 📖	CompOp	—
divisionMonoid 📖	CompOp	—
group 📖	CompOp	57 math math: Subgroup.mulSingle_mem_pi, oneLePart_apply, ProfiniteGrp.limit_one_val, Subgroup.pi_le_iff, Subgroup.pi_bot, Equiv.Perm.OnCycleFactors.kerParam_range_card, Subgroup.coe_pi, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, instGroupFG, Subgroup.pi_top, ProfiniteGrp.denseRange_toLimit, Subgroup.mem_pi, Subgroup.pi_empty, topologicalGroup, InfiniteGalois.mulEquivToLimit_symm_continuous, Subgroup.le_pi_iff, Subgroup.FG.pi, MeasureTheory.Measure.pi.isHaarMeasure, InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup, leOnePart_apply, Subgroup.pi_eq_bot_iff, InfiniteGalois.proj_adjoin_singleton_val, ProfiniteGrp.limit_mul_val, isNilpotent_pi_of_bounded_class, nilpotencyClass_pi, Subgroup.commutator_pi_pi_le, leOnePart_def, lowerCentralSeries_pi_le, Subgroup.index_pi, MeasureTheory.Measure.instIsHaarMeasureForallVolumeOfMeasurableMulOfSigmaFinite, Subgroup.closure_pi, CategoryTheory.ActionCategory.curry_apply_left, Equiv.Perm.sigmaCongrRightHom.card_range, instIsUniformGroup, MonoidHom.noncommPiCoprod_range, InfiniteGalois.toAlgEquivAux_eq_liftNormal, Equiv.Perm.OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_one, ProfiniteGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux, InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj, Int.subgroup_index_ne_zero_iff, ContinuousMap.coe_mabs, InfiniteGalois.mk_toAlgEquivAux, InfiniteGalois.proj_of_le, Equiv.Perm.OnCycleFactors.kerParam_range_le_centralizer, ProfiniteGrp.toLimitFun_continuous, InfiniteGalois.algEquivToLimit_continuous, oneLePart_def, CategoryTheory.ActionCategory.curry_apply_right, InfiniteGalois.limitToAlgEquiv_symm_apply, lowerCentralSeries_pi_of_finite, Equiv.Perm.OnCycleFactors.kerParam_range_eq, QuotientGroup.rightRel_pi, ProfiniteGrp.limit_ext_iff, Subgroup.commutator_pi_pi_of_finite, Subgroup.noncommPiCoprod_range, QuotientGroup.leftRel_pi, isNilpotent_pi
instSubtractionCommMonoid 📖	CompOp	—
invOneClass 📖	CompOp	—
involutiveInv 📖	CompOp	—
involutiveNeg 📖	CompOp	—
leftCancelMonoid 📖	CompOp	—
leftCancelSemigroup 📖	CompOp	—
monoid 📖	CompOp	30 math math: MulEquiv.val_piUnits_symm_apply, Monoid.exponent_pi, IsLocalization.isUnit_piRingHom_algebraMap_comp_piEvalRingHom, instSubsingletonUnits, MulEquiv.val_inv_piUnits_apply, ProbabilityTheory.sum_variance_truncation_le, instMonoidFG, ProbabilityTheory.variance_eq_sub, mulAutArrow_apply_apply, Finset.noncommProd_mulSingle, mulAutArrow_apply_symm_apply, ProbabilityTheory.condVar_ae_le_condExp_sq, isUnit_iff, orderOf, IsOfFinOrder.pi, analyticOrderAt_pow, orderOf_eq_sInf, threeGPFree_pi, orderOf_piMulSingle, Submonoid.FG.pi, ProbabilityTheory.variance_le_expectation_sq, instIsMulTorsionFree, Finset.noncommProd_mul_single, ProbabilityTheory.condVar_ae_eq_condExp_sq_sub_sq_condExp, MulEquiv.val_piUnits_apply, ConvexOn.pow, Matrix.isUnit_diagonal, orderOf_apply_dvd_orderOf, MulEquiv.val_inv_piUnits_symm_apply, Monoid.exponent_pi_eq_zero
mulOneClass 📖	CompOp	62 math math: Filter.Germ.coe_coeMulHom, ContMDiffMap.coeFnMonoidHom_apply, constMonoidHom_apply, MonoidHom.functions_ext'_iff, Function.ExtendByOne.hom_apply, PiTensorProduct.mapLMonoidHom_apply, Submonoid.coe_pi, Submonoid.mem_pi, Submonoid.pi_top, CategoryTheory.PreGaloisCategory.autEmbedding_injective, Submonoid.le_pi_iff, Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod, Equiv.Perm.OnCycleFactors.kerParam_injective, Submonoid.closure_pi, CommMonCat.coyonedaType_obj_map, MonoidHom.compLeft_apply, Submonoid.iSup_map_mulSingle_le, evalMonoidHom_apply, CommGrpCat.coyonedaType_map_app, LocallyConstant.coeFnMonoidHom_apply, MonoidHom.coeFn_apply, MonoidHom.noncommPiCoprod_apply, Subgroup.noncommPiCoprod_apply, MonoidHom.noncommPiCoprod_mulSingle, PiTensorProduct.tprodMonoidHom_apply, Submonoid.iSup_map_mulSingle, Submonoid.pi_le_iff, IsLocalization.iff_map_piEvalRingHom, Submonoid.le_comap_mulSingle_pi, Subgroup.injective_noncommPiCoprod_of_iSupIndep, PiTensorProduct.singleAlgHom_apply, MonoidHom.mulSingle_apply, Subgroup.noncommPiCoprod_mulSingle, monoidHom_apply, Equiv.Perm.sigmaCongrRightHom_injective, Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_apply, MonoidHom.coe_mulSingle, MonoidHom.noncommPiCoprod_mrange, MonoidHom.comp_noncommPiCoprod, BoundedContinuousFunction.coeFnMonoidHom_apply, Submonoid.pi_bot, Equiv.Perm.sigmaCongrRightHom_apply, CategoryTheory.PreGaloisCategory.autEmbedding_apply, coe_evalMonoidHom, CategoryTheory.PreGaloisCategory.autEmbedding_range, Submonoid.mulSingle_mem_pi, Submonoid.pi_eq_bot_iff, MonoidHom.injective_noncommPiCoprod_of_iSupIndep, CommGrpCat.coyonedaType_obj_map, PiTensorProduct.mapMonoidHom_apply, monoidHom_injective, Submonoid.pi_empty, MonoidHom.commute_noncommPiCoprod, instNatPowAssoc, Equiv.Perm.OnCycleFactors.kerParam_apply, IsDedekindDomain.selmerGroup.valuation_ker_eq, CommMonCat.coyonedaType_map_app, ContinuousMap.coeFnMonoidHom_apply, CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding, Equiv.Perm.commute_ofSubtype_noncommPiCoprod, Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply, CategoryTheory.PreGaloisCategory.autEmbedding_range_isClosed
negZeroClass 📖	CompOp	—
rightCancelMonoid 📖	CompOp	—
rightCancelSemigroup 📖	CompOp	—
semigroup 📖	CompOp	2 math math: pi_dvd_iff, instDecompositionMonoidForall
subNegMonoid 📖	CompOp	21 math math: BoundedContinuousFunction.coe_zsmul, LieModule.genWeightSpaceChain_def', LieModule.coe_chainTop, LieModuleHom.coe_zsmul, LieModule.exists_forall_mem_corootSpace_smul_add_eq_zero, CentroidHom.coe_intCast, Function.locallyFinsuppWithin.coe_zsmul, LieModule.exists₂_genWeightSpace_smul_add_eq_bot, LieModule.genWeightSpace_chainBotCoeff_sub_one_zsmul_sub, EisensteinSeries.finGcdMap_smul, LieModule.genWeightSpace_chainTopCoeff_add_one_zsmul_add, LieModule.genWeightSpace_le_genWeightSpaceChain, LieModule.genWeightSpaceChain_def, BoundedContinuousFunction.coe_zsmulRec, LieModule.coe_chainBot, Complex.ofReal_comp_zsmul, RootPairing.GeckConstruction.lie_e_lie_f_apply, DFinsupp.coe_zsmul, ContMDiffSection.coe_zsmul, RootPairing.GeckConstruction.e_lie_u, NormedAddGroupHom.coe_zsmul
subNegZeroMonoid 📖	CompOp	—
subtractionMonoid 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsCancelAdd 📖	mathematical	IsCancelAdd	instAdd	—	instIsLeftCancelAdd IsCancelAdd.toIsLeftCancelAdd instIsRightCancelAdd IsCancelAdd.toIsRightCancelAdd
instIsCancelMul 📖	mathematical	IsCancelMul	instMul	—	instIsLeftCancelMul IsCancelMul.toIsLeftCancelMul instIsRightCancelMul IsCancelMul.toIsRightCancelMul
instIsLeftCancelAdd 📖	mathematical	IsLeftCancelAdd	instAdd	—	add_left_cancel
instIsLeftCancelMul 📖	mathematical	IsLeftCancelMul	instMul	—	mul_left_cancel
instIsRightCancelAdd 📖	mathematical	IsRightCancelAdd	instAdd	—	add_right_cancel
instIsRightCancelMul 📖	mathematical	IsRightCancelMul	instMul	—	mul_right_cancel

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi_mulSingle_eq 📖	mathematical	—	Pi.mulSingle	—	Pi.mulSingle_eq_same
pi_single_eq 📖	mathematical	—	Pi.single	—	Pi.single_eq_same

Sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
elim_add_add 📖	mathematical	—	Pi.instAdd	—	—
elim_div_div 📖	mathematical	—	Pi.instDiv	—	—
elim_inv_inv 📖	mathematical	—	Pi.instInv	—	—
elim_mulSingle_one 📖	mathematical	—	Pi.mulSingle Pi.instOne	—	elim_update_left elim_one_one
elim_mul_mul 📖	mathematical	—	Pi.instMul	—	—
elim_neg_neg 📖	mathematical	—	Pi.instNeg	—	—
elim_one_mulSingle 📖	mathematical	—	Pi.instOne Pi.mulSingle	—	elim_update_right elim_one_one
elim_one_one 📖	mathematical	—	Pi.instOne	—	—
elim_single_zero 📖	mathematical	—	Pi.single Pi.instZero	—	elim_update_left elim_zero_zero
elim_sub_sub 📖	mathematical	—	Pi.instSub	—	—
elim_zero_single 📖	mathematical	—	Pi.instZero Pi.single	—	elim_update_right elim_zero_zero
elim_zero_zero 📖	mathematical	—	Pi.instZero	—	—

(root)

Definitions

Name	Category	Theorems
uniqueOfSurjectiveOne 📖	CompOp	—
uniqueOfSurjectiveZero 📖	CompOp	—

---

← Back to Index