| Name | Category | Theorems |
|---|
constr 📖 | CompOp | 18 mathmath: constr_comp, constr_symm_apply, coe_constrL, PowerBasis.constr_pow_algebraMap, PowerBasis.constr_pow_gen, constr_apply_fintype, Ideal.constr_basisSpanSingleton, toMatrix_eq_toMatrix_constr, constr_basis, PowerBasis.liftEquiv'_symm_apply_apply, PowerBasis.constr_pow_mul, constr_self, constr_def, SymmetricAlgebra.IsSymmetricAlgebra.mvPolynomial, constr_range, constr_apply, PowerBasis.constr_pow_aeval, constr_eq
|
coord 📖 | CompOp | 33 mathmath: dualBasis_coord_toDualEquiv_apply, mk_coord_apply_eq, coe_dualBasis, mk_coord_apply_ne, exists_basis_of_pairing_ne_zero, forall_coord_eq_zero_iff, coe_sumCoords_of_fintype, TensorProduct.dualDistribEquivOfBasis_symm_apply, flag_le_ker_coord, exists_basis_of_pairing_eq_zero, FGModuleCat.FGModuleCatCoevaluation_apply_one, coe_sumCoords_eq_finsum, toMatrix_dualTensorHom, exteriorPower.ιMultiDual_apply_ιMulti, sum_dual_apply_smul_coord, SmithNormalForm.le_ker_coord_of_notMem_range, exteriorPower.basis_coord, mk_coord_apply, TensorProduct.equivFinsuppOfBasisRight_apply, linearCombination_coord, coe_toDual_self, flag_le_ker_coord_iff, Basis.multilinearMap_apply, TensorProduct.equivFinsuppOfBasisLeft_apply, det_smul_mk_coord_eq_det_update, Complex.isometryOfOrthonormal_symm_apply, dvd_coord_smul, coord_unitsSMul, coord_apply, coord_equivFun_symm, SmithNormalForm.coord_apply_embedding_eq_smul_coord, coord_toDualEquiv_symm_apply, coord_repr_symm
|
equiv 📖 | CompOp | 9 mathmath: det_comp_basis, equiv_apply, equiv_trans, equiv_refl, map_equiv, equiv_symm, Orthonormal.equiv_toLinearEquiv, det_basis, LinearMap.toMatrix_basis_equiv
|
equiv' 📖 | CompOp | 2 mathmath: equiv'_symm_apply, equiv'_apply
|
equivFun 📖 | CompOp | 33 mathmath: equivFun_self, PiLp.basisFun_equivFun, map_equivFun, equivFun_symm_apply, ZLattice.covolume_eq_det_inv, IsBaseChange.of_fintype_basis_eq, continuous_equivFun_basis, star_dotProduct_toMatrix₂_mulVec, coe_toOrthonormalBasis_repr, constrL_apply, BilinForm.dotProduct_toMatrix_mulVec, equivFun_ofEquivFun, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, LinearMap.BilinForm.dotProduct_toMatrix_mulVec, dualBasis_equivFun, coe_toOrthonormalBasis_repr_symm, ofEquivFun_equivFun, constr_apply_fintype, parallelepiped_eq_map, ZLattice.volume_image_eq_volume_div_covolume, equivFun_apply, ZLattice.volume_image_eq_volume_div_covolume', Algebra.TensorProduct.equivPiOfFiniteBasis_symm_apply, OrthonormalBasis.coe_toBasis_repr, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply, Algebra.traceMatrix_of_basis_mulVec, Basis.equivFun_symm_single, Pi.basisFun_equivFun, sum_equivFun, Algebra.TensorProduct.equivPiOfFiniteBasis_apply, toDual_eq_equivFun, coord_equivFun_symm, dotProduct_toMatrix₂_mulVec
|
instFunLike 📖 | CompOp | 481 mathmath: NumberField.basisMatrix_eq_embeddingsMatrixReindex, KaehlerDifferential.mvPolynomialBasis_apply, det_comp_basis, equivFun_self, coe_map, coe_mapCoeffs, Ideal.selfBasis_def, mem_submodule_iff, Module.exists_basis_of_span_of_flat, tensorProduct_apply, tendsto_tsum_div_pow_atTop_integral, NumberField.canonicalEmbedding.mem_span_latticeBasis, Polynomial.Sequence.basis_natDegree_strictMono, NumberField.integralBasis_apply, exteriorPower.basis_apply, NumberField.Units.logEmbedding_fundSystem, Ideal.exists_smith_normal_form, ZSpan.volume_real_fundamentalDomain, QuadraticMap.sum_polar_sub_repr_sq, equivFun_symm_apply, range_ofVectorSpace, NumberField.canonicalEmbedding.latticeBasis_apply, TensorProduct.equivFinsuppOfBasisLeft_symm_apply, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, toDual_linearCombination_left, constr_symm_apply, LinearMap.BilinForm.toMatrixAux_eq, Algebra.Generators.cotangentSpaceBasis_apply, mem_span, PeriodPair.basis_one, LinearMap.toMatrix_apply', constrL_basis, exteriorPower.coe_basis, TensorProduct.sum_tmul_basis_right_injective, WeierstrassCurve.Affine.CoordinateRing.basis_one, IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow, IsCyclotomicExtension.discr_odd_prime, exteriorPower.basis_repr_ne, Field.Emb.Cardinal.filtration_succ, ofZLatticeBasis_apply, IsBaseChange.of_fintype_basis_eq, Polynomial.Sequence.basis_eq_self, BoxIntegral.unitPartition.mem_smul_span_iff, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, isUnit_det, ZSpan.smul, flag_le_ker_dual, ofZLatticeComap_apply, coe_mkFinConsOfLE, coe_dualBasis, coe_extendLe, WeierstrassCurve.Affine.CoordinateRing.coe_basis, repr_self_apply, Algebra.discr_eq_discr, Polynomial.degreeLT.basis_val, Algebra.Generators.exists_presentation_of_basis_cotangent, LinearMap.sum_repr_mul_repr_mulₛₗ, Algebra.TensorProduct.basis_apply, equiv_apply, FiniteDimensional.basisSingleton_apply, Module.DualBases.coe_dualBasis, ofSpan_subset, Algebra.traceMatrix_localizationLocalization, LDL.lowerInv_eq_gramSchmidtBasis, det_isUnitSMul, LinearMap.exists_basis_basis_of_span_eq_top_of_mem_algebraMap, DirectSum.IsInternal.collectedBasis_mem, eq_of_apply_eq_iff, AlternatingMap.map_basis_eq_zero_iff, ModN.basis_apply_eq_mkQ, coe_basisOfOrthonormalOfCardEqFinrank, BoxIntegral.unitPartition.integralSum_eq_tsum_div, toLin_toMatrix, mulOpposite_apply, PeriodPair.latticeBasis_zero, LinearMap.toMatrixAlgEquiv_apply, maximal, mem_center_iff, LinearMap.BilinForm.apply_dualBasis_left, tendsto_card_div_pow_atTop_volume, extendLe_subset, mulOpposite_is_orthonormal_iff, mk_range_eq_rank, prod_apply_inr_fst, Field.Emb.Cardinal.two_le_deg, exteriorPower.ιMultiDual_apply_diag, Algebra.SubmersivePresentation.basisKaehlerOfIsCompl_apply, le_span, IsCyclotomicExtension.Rat.discr_prime_pow', DirectSum.IsInternal.collectedBasis_coe, LinearMap.eq_adjoint_iff_basis_left, mk_apply, prod_apply_inl_snd, ZSpan.quotientEquiv_apply_mk, Field.Emb.Cardinal.isLeast_leastExt, Pi.basis_repr_single, Algebra.traceMatrix_reindex, Algebra.Generators.exists_presentation_of_free_cotangent, AddSubgroup.index_eq_natAbs_det, sumQuot_repr_left, Polynomial.degreeLT.addLinearEquiv_castAdd, Field.Emb.Cardinal.succEquiv_coherence, Algebra.discr_powerBasis_eq_norm, coe_basisOfPiSpaceOfLinearIndependent, TensorProduct.equivFinsuppOfBasisLeft_symm, reindexRange_apply, matrix_apply, exists_basis_of_pairing_ne_zero, localizationLocalization_apply, TensorAlgebra.equivFreeAlgebra_symm_ι, reindexFinsetRange_apply, LinearMap.BilinForm.dualSubmodule_span_of_basis, NumberField.Units.span_basisOfIsMaxRank, orientation_eq_iff_det_pos, IsNoetherian.range_finsetBasis, ZSpan.measureReal_fundamentalDomain, NumberField.Units.basisOfIsMaxRank_apply, linearMap_apply, PeriodPair.basis_zero, coe_basisOfTopLeSpanOfCardEqFinrank, trace_traceDual_mul, Pi.basis_apply, MonoidAlgebra.basis_apply, ZSpan.repr_ceil_apply, end_apply_apply, PowerBasis.coe_basis, Algebra.traceForm_toMatrix, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, LinearMap.BilinForm.dualSubmodule_dualSubmodule_flip_of_basis, ZSpan.volume_fundamentalDomain, basis_toMatrix_basisFun_mul, NumberField.det_basisOfFractionalIdeal_eq_absNorm, ZSpan.measure_fundamentalDomain, TensorAlgebra.equivFreeAlgebra_ι_apply, range_extendLe, trace_mul_traceDual, reindexRange_repr_self, IntermediateField.LinearDisjoint.basisOfBasisLeft_apply, subset_extendLe, QuadraticMap.toBilin_apply, repr_eq_iff, LinearMap.BilinForm.toMatrix_apply, maximal_orthonormal_iff_basis_of_finiteDimensional, TensorProduct.dualDistribEquivOfBasis_symm_apply, coe_algebraMapCoeffs, IsBaseChange.of_basis, Field.Emb.Cardinal.instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, NumberField.mixedEmbedding.span_idealLatticeBasis, IntermediateField.LinearDisjoint.basisOfBasisRight_apply, repr_linearCombination, dualBasis_apply_self, NumberField.Units.fundSystem_mk, span_apply, LinearMap.toMatrix_reindexRange, exists_basis_of_pairing_eq_zero, dualBasis_equivFun, Basis.ofRankEqZero_apply, prod_apply, coe_smul, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_eq, ofZLatticeBasis_span, linearCombination_dualBasis, NumberField.mixedEmbedding.mem_span_latticeBasis, IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one, IsGalois.normalBasis_apply, Matrix.toLin_self, SmithNormalForm.snf, LinearMap.BilinForm.sum_repr_mul_repr_mul, hasEigenvector_toLin'_diagonal, Matrix.GeneralLinearGroup.toLin'_apply, BilinearForm.toMatrixAux_eq, IsLocalFrameOn.toBasisAt_coe, LinearMap.BilinForm.exists_orthogonal_basis, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_eq, FGModuleCat.FGModuleCatCoevaluation_apply_one, IsBaseChange.of_fintype_basis, range_extend, Algebra.embeddingsMatrixReindex_eq_vandermonde, ofIsLocalizedModule_apply, coe_basisOfLinearIndependentOfCardEqFinrank, isUnitSMul_apply, LinearMap.BilinForm.dualBasis_repr_apply, PiLp.basisFun_apply, end_apply, MvPolynomial.coe_basisMonomials, Subalgebra.adjoin_eq_span_basis, Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_apply, repr_symm_single, PiTensorProduct.dualDistribInvOfBasis_apply, NumberField.discr_eq_discr, restrictScalars_repr_apply, IsCyclotomicExtension.Rat.discr_prime_pow_ne_two', NumberField.Units.regOfFamily_of_isMaxRank, injective, FiniteDimensional.range_basisSingleton, coe_singleton, ZSpan.coe_floor_self, InnerProductSpace.coe_gramSchmidtBasis, linearMap_toMatrix_mul_basis_toMatrix, coe_reindex, instIsZLatticeRealSpan, LinearMap.toMatrix_transpose_apply, toMatrix_dualTensorHom, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, IsCyclotomicExtension.discr_prime_pow_ne_two, restrictScalars_apply, flag_succ, InnerProductSpace.gramSchmidt_triangular, mem_submodule_iff', Submodule.smithNormalFormBotBasis_def, sum_dual_apply_smul_coord, toDual_eq_repr, baseChange_end, sum_repr_mul_repr, LinearMap.BilinForm.dualBasis_eq_iff, baseChange_apply, ZSpan.isAddFundamentalDomain', Algebra.TensorProduct.basis_repr_symm_apply', ZSpan.norm_fract_le, mul_basis_toMatrix, OrthonormalBasis.coe_toBasis, LinearMap.BilinForm.dualSubmodule_dualSubmodule_of_basis, PowerBasis.toMatrix_isIntegral, RootPairing.Base.toCoweightBasis_apply, parallelepiped_basis_eq, mem_span_image, dualBasis_apply, Ideal.basisSpanSingleton_apply, sum_toMatrix_smul_self, PowerBasis.basis_eq_pow, ZSpan.span_top, reindexFinsetRange_repr_self, Algebra.discr_mul_isIntegral_mem_adjoin, LinearMap.toMatrix_transpose_apply', repr_symm_single_one, NumberField.mixedEmbedding.span_latticeBasis, extend_apply_self, AlternatingMap.eq_smul_basis_det, Finsupp.coe_basis, LinearMap.toMatrix_smulRight, LinearMap.toMatrix₂Aux_eq, ZSpan.map, Polynomial.degreeLT.addLinearEquiv_symm_apply_inr_basis, ZSpan.exist_unique_vadd_mem_fundamentalDomain, ZSpan.fundamentalDomain_subset_parallelepiped, Module.exists_basis_of_span_of_maximalIdeal_rTensor_injective, Basis.multilinearMap_apply_apply, BilinForm.toMatrix_mul_basis_toMatrix, SymmetricAlgebra.equivMvPolynomial_symm_X, coe_parallelepiped, PeriodPair.latticeBasis_one, ZLattice.covolume_eq_det_mul_measureReal, ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite, ZSpan.isAddFundamentalDomain, Algebra.toMatrix_lmul', coe_ofVectorSpace, map_apply, Field.Emb.Cardinal.filtration_apply, Matrix.toLin_apply, coe_mk, Submodule.exists_smith_normal_form_of_rank_eq, smulTower'_apply, Basis.mem_ideal_iff', Polynomial.coe_basisMonomials, Finsupp.coe_basisSingleOne, sumCoords_self_apply, SymmetricAlgebra.equivMvPolynomial_ι_apply, Algebra.discr_powerBasis_eq_prod, Ideal.constr_basisSpanSingleton, Matrix.IsHermitian.eigenvectorUnitary_coe, Algebra.traceMatrix_of_basis, Field.Emb.Cardinal.deg_lt_aleph0, TensorProduct.eq_repr_basis_left, end_repr_symm_apply, range_ofSpan, toMatrix_mul_toMatrix_flip, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, apply_eq_iff, LinearMap.eq_adjoint_iff_basis, Matrix.stdBasis_eq_single, det_self, Algebra.Generators.disjoint_ker_toKaehler_of_linearIndependent, OrthonormalBasis.orthonormal_adjustToOrientation, LinearMap.BilinForm.toMatrix_mul_basis_toMatrix, Matrix.toLinAlgEquiv_apply, coe_ofRepr, linearIndependent, self_mem_flag_iff, det_basis, mapCoeffs_apply, Algebra.SubmersivePresentation.basisCotangent_localizationAway_apply, det_inv, self_mem_span_image, Algebra.Generators.repr_CotangentSpaceMap, dualBasis_repr, TensorProduct.dualDistribInvOfBasis_apply, smulTower_apply, linearCombination_repr, Field.Emb.Cardinal.strictMono_filtration, BilinForm.toMatrix_apply, linearCombination_coord, toDual_apply, Algebra.Generators.toKaehler_cotangentSpaceBasis, ZSpan.quotientEquiv.symm_apply, NumberField.mem_span_integralBasis, RootPairing.Base.toWeightBasis_apply, coe_repr_symm, Algebra.discr_isUnit_of_basis, coe_setBasisOfLinearIndependentOfCardEqFinrank, Algebra.SubmersivePresentation.basisKaehler_apply, Submodule.eq_top_iff_forall_basis_mem, PiLp.basis_toMatrix_basisFun_mul, Pi.basisFun_apply, Matrix.toLinAlgEquiv_self, NumberField.mem_span_basisOfFractionalIdeal, coe_toDual_self, LinearMap.toMatrix₂_mul_basis_toMatrix, Basis.mem_ideal_iff, IsBaseChange.basis_apply, ZSpan.instDiscreteTopologySubtypeMemAddSubgroupToAddSubgroupIntSpanRangeCoeBasisRealOfFinite, NumberField.mixedEmbedding.latticeBasis_apply, sumQuot_inr, flag_le_iff, Subalgebra.LinearDisjoint.basisOfBasisLeft_apply, AddMonoidAlgebra.basis_apply, IsLocalRing.basisQuotient_apply, Orientation.coe_basisRightAngleRotation, localizationLocalization_span, Algebra.discr_localizationLocalization, linearMap_apply_apply, toMatrix_isUnitSMul, coe_finsetBasisOfLinearIndependentOfCardEqFinrank, LinearMap.toMatrix₂_apply, ofVectorSpace_apply_self, algebraMapCoeffs_apply, WeierstrassCurve.Affine.CoordinateRing.basis_zero, Field.Emb.Cardinal.iSup_adjoin_eq_top, repr_sum_self, self_mem_flag, LinearMap.BilinForm.dualSubmodule_flip_dualSubmodule_of_basis, AlternatingMap.measure_def, linearMap_repr_symm_apply, constr_basis, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, adjustToOrientation_apply_eq_or_eq_neg, finTwoProd_zero, FractionalIdeal.abs_det_basis_change, det_mul_det, toDual_linearCombination_right, Matrix.toLinearMapₛₗ₂_apply_basis, FiniteDimensional.exists_is_basis_integral, LinearMap.toMatrix_toSpanSingleton, Polynomial.degreeLT.addLinearEquiv_natAdd, singleton_apply, TensorProduct.equivFinsuppOfBasisRight_symm, Field.Emb.Cardinal.adjoin_image_leastExt, exteriorPower.basis_repr, Algebra.discr_powerBasis_eq_prod'', Algebra.traceMatrix_of_basis_mulVec, Basis.multilinearMap_apply, Field.Emb.Cardinal.instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, ZSpan.discreteTopology_pi_basisFun, traceDual_repr_apply, range_reindex, Polynomial.degreeLT.addLinearEquiv_symm_apply_inl_basis, prod_apply_inl_fst, NumberField.basisOfFractionalIdeal_apply, ofSpan_apply_self, extendLe_apply_self, basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix, Algebra.discr_powerBasis_eq_prod', smul_apply, tendsto_card_div_pow_atTop_volume', Algebra.IsStandardSmooth.iff_exists_basis_kaehlerDifferential, tensorProduct_apply', LinearMap.eq_adjoint_iff_basis_right, ofIsLocalizedModule_span, LinearMap.toMatrixAlgEquiv_apply', Basis.equivFun_symm_single, AddSubgroup.relIndex_eq_natAbs_det, LinearMap.isSymm_iff_basis, constr_self, ZSpan.vadd_mem_fundamentalDomain, exteriorPower.ιMultiDual_apply_nondiag, traceDual_powerBasis_eq, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, ZSpan.fract_apply, toDual_apply_left, AddChar.coe_complexBasis, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, Matrix.toLinearMap₂_apply_basis, coe_mkFinCons, extendOfIsLattice_apply, IsCyclotomicExtension.Rat.discr_odd_prime', span_eq, Polynomial.degreeLT.basisProd_natAdd, det_unitsSMul_self, toDual_apply_right, NumberField.coe_discr, ZSpan.repr_floor_apply, repr_symm_apply, basis_toMatrix_mul_linearMap_toMatrix, exteriorPower.ιMulti_family_linearIndependent_ofBasis, coe_ofEquivFun, Module.DualBases.coe_basis, LinearMap.toMatrixAlgEquiv_reindexRange, NumberField.mixedEmbedding.disjoint_span_commMap_ker, sum_equivFun, Field.Emb.Cardinal.adjoin_basis_eq_top, AddChar.complexBasis_apply, ZSpan.fract_eq_fract, ofIsCoprimeDifferentIdeal_apply, Complex.coe_basisOneI, Polynomial.Sequence.basis_degree_strictMono, sumQuot_inl, ZLattice.sum_piFinset_Icc_rpow_le, Module.exists_basis_of_basis_baseChange, Algebra.SubmersivePresentation.basisCotangent_apply, coe_extend, repr_eq_iff', mk_eq_spanRank, LinearMap.BilinForm.isSymm_iff_basis, toMatrix_self, PeriodPair.lattice_eq_span_range_basis, basis_toMatrix_mul, Ideal.natAbs_det_basis_change, unitsSMul_apply, mem_span_repr_support, toMatrix_mul_toMatrix, Algebra.leftMulMatrix_eq_repr_mul, toDual_eq_equivFun, Polynomial.degreeLT.basisProd_castAdd, sum_repr, toMatrix_mulVec_repr, Algebra.Generators.basisCotangentAway_apply, TensorProduct.sum_tmul_basis_left_injective, Submodule.basis_of_pid_aux, TensorProduct.equivFinsuppOfBasisRight_symm_apply, toMatrix_unitsSMul, prod_apply_inr_snd, mem_span_iff_repr_mem, hasEigenvector_toLin_diagonal, addHaar_self, toMatrix_map_vecMul, LinearMap.toMatrixAlgEquiv_transpose_apply, repr_self, QuadraticMap.basisRepr_apply, Basis.piTensorProduct_apply, WeierstrassCurve.Affine.CoordinateRing.basis_apply, ZSpan.setFinite_inter, reindex_apply, Submodule.exists_smith_normal_form_of_le, LinearMap.toMatrix_apply, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, restrictScalars_toMatrix, Module.FinitePresentation.exists_basis_localizedModule_powers, LinearMap.toMatrix_id_eq_basis_toMatrix, LinearMap.toMatrixAlgEquiv_transpose_apply', finTwoProd_one, Algebra.SubmersivePresentation.basisDeriv_apply, exteriorPower.basis_repr_self, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow', baseChange_linearMap, IsCyclotomicExtension.discr_prime_pow, ZSpan.fundamentalDomain_ae_parallelepiped, groupSMul_apply, BoxIntegral.unitPartition.tag_mem_smul_span, LinearMap.BilinForm.apply_dualBasis_right, ZLattice.covolume_eq_det, LinearMap.sum_repr_mul_repr_mul, coe_ofSpan, IsAdjoinRootMonic.basis_one, IsCyclotomicExtension.discr_prime_pow_ne_two', Submodule.natAbs_det_basis_change, traceDual_eq_iff, Algebra.discr_reindex, Trivialization.localFrame_apply_of_mem_baseSet, IsAdjoinRootMonic.basis_apply, AffineBasis.basisOf_apply, TensorProduct.eq_repr_basis_right
|
instInhabitedFinsupp 📖 | CompOp | — |
map 📖 | CompOp | 25 mathmath: coe_map, map_equivFun, PowerBasis.map_basis, map_repr, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, toMatrix_map, map_equiv, OrthonormalBasis.toBasis_map, Orthonormal.map_equiv, det_map', orientation_comp_linearEquiv_eq_iff_det_pos, orientation_comp_linearEquiv_eq_neg_iff_det_neg, ZSpan.map, Pi.orthonormalBasis.toBasis, map_apply, smul_eq_map, PiLp.basisFun_eq_pi_basisFun, parallelepiped_map, ZSpan.map_fundamentalDomain, Orthonormal.mapLinearIsometryEquiv, ofZLatticeBasis_comap, map_addHaar, PiLp.basisFun_map, det_map, orientation_map
|
mapCoeffs 📖 | CompOp | 3 mathmath: coe_mapCoeffs, mapCoeffs_apply, mapCoeffs_repr
|
ofEquivFun 📖 | CompOp | 4 mathmath: ofEquivFun_repr_apply, equivFun_ofEquivFun, ofEquivFun_equivFun, coe_ofEquivFun
|
reindex 📖 | CompOp | 26 mathmath: Polynomial.toMatrix_sylvesterMap', det_reindex', parallelepiped_reindex, reindex_refl, Algebra.traceMatrix_reindex, map_equiv, NumberField.det_basisOfFractionalIdeal_eq_absNorm, addHaar_reindex, det_reindex_symm, AffineBasis.basisOf_reindex, repr_reindex, coe_reindex, Orthonormal.map_equiv, det_reindex, ZSpan.fundamentalDomain_reindex, NumberField.inverse_basisMatrix_mulVec_eq_repr, OrthonormalBasis.reindex_toBasis, sumCoords_reindex, toMatrix_reindex, range_reindex, toMatrix_reindex', NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, reindex_apply, repr_reindex_apply, NumberField.house.basis_repr_norm_le_const_mul_house, orientation_reindex
|
reindexFinsetRange 📖 | CompOp | 4 mathmath: reindexFinsetRange_apply, reindexFinsetRange_repr_self, reindexFinsetRange_repr, reindexFinsetRange_self
|
reindexRange 📖 | CompOp | 7 mathmath: reindexRange_self, reindexRange_repr', reindexRange_repr, reindexRange_apply, reindexRange_repr_self, LinearMap.toMatrix_reindexRange, LinearMap.toMatrixAlgEquiv_reindexRange
|
repr 📖 | CompOp | 227 mathmath: end_repr_apply, Algebra.Presentation.differentials.comm₁₂_single, QuadraticMap.sum_polar_sub_repr_sq, Module.basisUnique_repr_eq_zero_iff, NumberField.Units.fun_eq_repr, IsBaseChange.basis_repr_comp_apply, Module.DualBases.basis_repr_symm_apply, IsAdjoinRootMonic.coeff_apply, LinearMap.toMatrix_apply', Matrix.repr_toLin, KaehlerDifferential.mvPolynomialBasis_repr_D_X, exteriorPower.basis_repr_ne, Algebra.Presentation.differentials.comm₂₃, mk_repr, repr_isUnitSMul, prod_repr_inl, repr_self_apply, IsLocalFrameOn.coeff_apply_of_mem, setBasisOfLinearIndependentOfCardEqFinrank_repr_apply, LinearMap.sum_repr_mul_repr_mulₛₗ, IntermediateField.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply, repr_algebraMap, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, Finsupp.basis_repr, Matrix.toBilin_apply, IsLocalRing.basisQuotient_repr, map_repr, LinearMap.toMatrixAlgEquiv_apply, Algebra.TensorProduct.basis_repr_tmul, NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd, LinearMap.BilinForm.apply_eq_dotProduct_toMatrix_mulVec, IsAdjoinRootMonic.basis_repr, Pi.basis_repr_single, TensorProduct.equivFinsuppOfBasisRight_apply_tmul, ofEquivFun_repr_apply, sumQuot_repr_left, reindexRange_repr', reindexRange_repr, TensorProduct.equivFinsuppOfBasisLeft_apply_tmul, repr_smul, NumberField.canonicalEmbedding.integralBasis_repr_apply, basisOfLinearIndependentOfCardEqFinrank_repr_apply, SmithNormalForm.repr_apply_embedding_eq_repr_smul, LinearMap.polyCharpolyAux_map_eval, ZSpan.repr_ceil_apply, addSubgroupOfClosure_repr_apply, repr_range, basis_toMatrix_basisFun_mul, reindexRange_repr_self, repr_eq_iff, sumQuot_repr_inl, Algebra.Generators.cotangentSpaceBasis_repr_tmul, Algebra.TensorProduct.equivFinsuppOfBasis_apply, repr_linearCombination, Algebra.TensorProduct.equivFinsuppOfBasis_symm_apply, PiLp.basisFun_repr, Algebra.Generators.H1Cotangent.δAux_toAlgHom, TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, FiniteDimensional.basisSingleton_repr_apply, equivFunL_symm_apply_repr, PowerBasis.repr_gen_pow_isIntegral, Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, LinearMap.BilinForm.sum_repr_mul_repr_mul, mulOpposite_repr_op, smulTower'_repr_mk, Matrix.GeneralLinearGroup.toLin'_apply, repr_reindex, algebraMapCoeffs_repr_apply_toFun, LinearMap.toMatrix_mulVec_repr, Matrix.toLin_apply_eq_zero_iff, algebraMapCoeffs_repr_apply_apply, Matrix.toLinearMapₛₗ₂_apply, LinearMap.BilinForm.dualBasis_repr_apply, sumQuot_repr_inl_of_mem, repr_symm_single, apply_eq_dotProduct_toMatrix₂_mulVec, finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply, restrictScalars_repr_apply, equivFunL_apply, Algebra.TensorProduct.basisAux_tmul, singleton_repr, LinearMap.polyCharpolyAux_map_eq_charpoly, LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff, LinearMap.toMatrix_transpose_apply, Pi.basis_repr, Algebra.Presentation.differentials.comm₂₃', InnerProductSpace.gramSchmidt_triangular, QuadraticAlgebra.basis_repr_apply, toDual_eq_repr, sum_repr_mul_repr, NumberField.integralBasis_repr_apply, linearMap_repr_apply, mem_span_image, NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst, localizationLocalization_repr_algebraMap, dualBasis_apply, apply_eq_star_dotProduct_toMatrix₂_mulVec, Complex.coe_basisOneI_repr, reindexFinsetRange_repr_self, LinearMap.toMatrix_transpose_apply', repr_symm_single_one, LinearMap.toMatrix_smulRight, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, RootPairing.Base.toCoweightBasis_repr_coroot, AdjoinRoot.powerBasisAux'_repr_symm_apply, Basis.multilinearMap_apply_apply, coe_finTwoProd_repr, IsAdjoinRootMonic.coeff_apply_lt, DirectSum.IsInternal.collectedBasis_repr_of_mem_ne, toMatrix_apply, KaehlerDifferential.mvPolynomialBasis_repr_apply, Module.DualBases.basis_repr_apply, Algebra.toMatrix_lmul', symmetricAlgebra_repr_apply, ZLattice.exists_forall_abs_repr_le_norm, Matrix.toLin_apply, Algebra.Presentation.differentials.comm₁₂, sumQuot_repr_inr_of_mem, repr_injective, repr_apply_eq, LinearMap.polyCharpolyAux_map_aeval, NumberField.inverse_basisMatrix_mulVec_eq_repr, end_repr_symm_apply, InnerProductSpace.toMatrix_rankOne, apply_eq_iff, setBasisOfTopLeSpanOfCardEqFinrank_repr_apply, LinearMap.polyCharpolyAux_coeff_eval, Matrix.toLinAlgEquiv_apply, Matrix.toLinearMap₂_apply, ZLattice.abs_repr_lt_of_norm_lt, Algebra.Generators.repr_CotangentSpaceMap, dualBasis_repr, NumberField.mixedEmbedding.stdBasis_apply_isReal, linearCombination_repr, union_support_maximal_linearIndependent_eq_range_basis, tensorAlgebra_repr_apply, equivFun_apply, mulOpposite_repr_eq, coe_repr_symm, smulTower'_repr, exteriorPower.basis_repr_apply, toMatrix_update, PiLp.basis_toMatrix_basisFun_mul, baseChange_repr_tmul, ZSpan.repr_fract_apply, Algebra.TensorProduct.basis_repr_symm_apply, LinearMap.polyCharpoly_map_eq_charpoly, QuaternionAlgebra.coe_basisOneIJK_repr, NumberField.mixedEmbedding.latticeBasis_repr_apply, ext_elem_iff, KaehlerDifferential.mvPolynomialBasis_repr_D, repr_sum_self, RootPairing.Base.toWeightBasis_repr_root, Algebra.leftMulMatrix_mulVec_repr, Finsupp.basisSingleOne_repr, smulTower_repr_mk, repr_support_subset_of_mem_span, linearMap_repr_symm_apply, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, SmithNormalForm.repr_comp_embedding_eq_smul, LinearMap.toMatrix_toSpanSingleton, exteriorPower.basis_repr, IsBaseChange.basis_repr_comp, OrthonormalBasis.coe_toBasis_repr_apply, ZLattice.normBound_spec, AdjoinRoot.powerBasisAux'_repr_apply_to_fun, IsAdjoinRootMonic.coeff_apply_coe, mapCoeffs_repr, traceDual_repr_apply, ofZLatticeComap_repr_apply, LinearMap.toMvPolynomial_eval_eq_apply, KaehlerDifferential.mvPolynomialBasis_repr_symm_single, toMatrix_transpose_apply, ofZLatticeBasis_repr_apply, LinearMap.toMatrixAlgEquiv_apply', IntermediateField.LinearDisjoint.basisOfBasisLeft_repr_apply, prod_repr_inr, BilinForm.apply_eq_dotProduct_toMatrix_mulVec, constr_def, toDual_apply_left, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, reindexFinsetRange_repr, continuous_coe_repr, smulTower_repr, toDual_apply_right, ZSpan.repr_floor_apply, repr_symm_apply, tensorProduct_repr_tmul_apply, Basis.piTensorProduct_repr_tprod_apply, repr_smul', repr_unitsSMul, constr_apply, Subalgebra.LinearDisjoint.basisOfBasisLeft_repr_apply, repr_eq_iff', norm_repr_le_norm, mem_span_repr_support, Pi.basisFun_repr, Algebra.leftMulMatrix_eq_repr_mul, sum_repr, ZSpan.mem_fundamentalDomain, toMatrix_mulVec_repr, finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply, algebraMapCoeffs_repr, coord_apply, mem_span_iff_repr_mem, SmithNormalForm.repr_eq_zero_of_notMem_range, LinearMap.toMatrixAlgEquiv_transpose_apply, repr_self, Polynomial.degreeLT.basis_repr, repr_reindex_apply, LinearMap.toMatrix_apply, NumberField.house.basis_repr_norm_le_const_mul_house, LinearMap.toMatrixAlgEquiv_transpose_apply', LinearMap.polyCharpoly_coeff_eval, repr_unop_eq_mulOpposite_repr, exteriorPower.basis_repr_self, sumQuot_repr_inr, coord_repr_symm, ZLattice.abs_repr_le, DirectSum.IsInternal.collectedBasis_repr_of_mem, coe_sumCoords, LinearMap.sum_repr_mul_repr_mul, ofIsLocalizedModule_repr_apply, LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly
|
sumCoords 📖 | CompOp | 6 mathmath: AffineBasis.linear_eq_sumCoords, coe_sumCoords_of_fintype, coe_sumCoords_eq_finsum, sumCoords_self_apply, sumCoords_reindex, coe_sumCoords
|