Basis 📖 | CompData | 510 mathmath: NumberField.basisMatrix_eq_embeddingsMatrixReindex, KaehlerDifferential.mvPolynomialBasis_apply, Basis.det_comp_basis, Basis.equivFun_self, Basis.coe_map, Basis.coe_mapCoeffs, Basis.instIsScalarTower, Ideal.selfBasis_def, Basis.mem_submodule_iff, exists_basis_of_span_of_flat, Basis.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, free_iff_set, Basis.equivFun_symm_apply, Basis.range_ofVectorSpace, NumberField.canonicalEmbedding.latticeBasis_apply, TensorProduct.equivFinsuppOfBasisLeft_symm_apply, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, Basis.toDual_linearCombination_left, Basis.constr_symm_apply, LinearMap.BilinForm.toMatrixAux_eq, Algebra.Generators.cotangentSpaceBasis_apply, Basis.mem_span, PeriodPair.basis_one, LinearMap.toMatrix_apply', Basis.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, Basis.basis_singleton_iff, exteriorPower.basis_repr_ne, Field.Emb.Cardinal.filtration_succ, Basis.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, Basis.isUnit_det, finrank_eq_one_iff, ZSpan.smul, Basis.flag_le_ker_dual, Basis.ofZLatticeComap_apply, Basis.coe_mkFinConsOfLE, Basis.coe_dualBasis, Algebra.smul_leftMulMatrix, Basis.coe_extendLe, WeierstrassCurve.Affine.CoordinateRing.coe_basis, 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, Basis.equiv_apply, FiniteDimensional.basisSingleton_apply, DualBases.coe_dualBasis, Basis.ofSpan_subset, Algebra.traceMatrix_localizationLocalization, LDL.lowerInv_eq_gramSchmidtBasis, Basis.det_isUnitSMul, LinearMap.exists_basis_basis_of_span_eq_top_of_mem_algebraMap, DirectSum.IsInternal.collectedBasis_mem, Basis.eq_of_apply_eq_iff, AlternatingMap.map_basis_eq_zero_iff, ModN.basis_apply_eq_mkQ, coe_basisOfOrthonormalOfCardEqFinrank, BoxIntegral.unitPartition.integralSum_eq_tsum_div, Basis.toLin_toMatrix, Basis.mulOpposite_apply, PeriodPair.latticeBasis_zero, LinearMap.toMatrixAlgEquiv_apply, Basis.maximal, Basis.mem_center_iff, LinearMap.BilinForm.apply_dualBasis_left, tendsto_card_div_pow_atTop_volume, Basis.extendLe_subset, Basis.mulOpposite_is_orthonormal_iff, Basis.mk_range_eq_rank, Basis.prod_apply_inr_fst, Field.Emb.Cardinal.two_le_deg, exteriorPower.ιMultiDual_apply_diag, Algebra.SubmersivePresentation.basisKaehlerOfIsCompl_apply, Basis.le_span, IsCyclotomicExtension.Rat.discr_prime_pow', DirectSum.IsInternal.collectedBasis_coe, LinearMap.eq_adjoint_iff_basis_left, Basis.mk_apply, Basis.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, Basis.sumQuot_repr_left, Polynomial.degreeLT.addLinearEquiv_castAdd, Field.Emb.Cardinal.succEquiv_coherence, Algebra.discr_powerBasis_eq_norm, coe_basisOfPiSpaceOfLinearIndependent, TensorProduct.equivFinsuppOfBasisLeft_symm, LinearMap.det_def, Basis.reindexRange_apply, Basis.matrix_apply, exists_basis_of_pairing_ne_zero, Basis.localizationLocalization_apply, TensorAlgebra.equivFreeAlgebra_symm_ι, Basis.reindexFinsetRange_apply, AffineBasis.basisOf_smul, LinearMap.detAux_def, LinearMap.BilinForm.dualSubmodule_span_of_basis, NumberField.Units.span_basisOfIsMaxRank, Basis.repr_smul, Basis.orientation_eq_iff_det_pos, IsNoetherian.range_finsetBasis, ZSpan.measureReal_fundamentalDomain, NumberField.Units.basisOfIsMaxRank_apply, Basis.linearMap_apply, PeriodPair.basis_zero, coe_basisOfTopLeSpanOfCardEqFinrank, Basis.trace_traceDual_mul, Pi.basis_apply, MonoidAlgebra.basis_apply, ZSpan.repr_ceil_apply, Basis.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, Basis.range_extendLe, Basis.trace_mul_traceDual, Basis.reindexRange_repr_self, IntermediateField.LinearDisjoint.basisOfBasisLeft_apply, Basis.subset_extendLe, Basis.smul_det, QuadraticMap.toBilin_apply, Basis.repr_eq_iff, LinearMap.BilinForm.toMatrix_apply, maximal_orthonormal_iff_basis_of_finiteDimensional, TensorProduct.dualDistribEquivOfBasis_symm_apply, Basis.coe_algebraMapCoeffs, IsBaseChange.of_basis, Field.Emb.Cardinal.instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, NumberField.mixedEmbedding.span_idealLatticeBasis, IntermediateField.LinearDisjoint.basisOfBasisRight_apply, Basis.repr_linearCombination, Basis.dualBasis_apply_self, NumberField.Units.fundSystem_mk, Basis.span_apply, LinearMap.toMatrix_reindexRange, exists_basis_of_pairing_eq_zero, Basis.dualBasis_equivFun, Basis.ofRankEqZero_apply, LinearMap.toMatrix_smulBasis_left, Basis.prod_apply, Basis.coe_smul, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_eq, Basis.ofZLatticeBasis_span, Basis.linearCombination_dualBasis, NumberField.mixedEmbedding.mem_span_latticeBasis, IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one, IsGalois.normalBasis_apply, Matrix.toLin_self, Basis.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, Basis.range_extend, Algebra.embeddingsMatrixReindex_eq_vandermonde, Basis.ofIsLocalizedModule_apply, coe_basisOfLinearIndependentOfCardEqFinrank, Basis.isUnitSMul_apply, LinearMap.BilinForm.dualBasis_repr_apply, PiLp.basisFun_apply, Basis.end_apply, MvPolynomial.coe_basisMonomials, Subalgebra.adjoin_eq_span_basis, Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_apply, Basis.repr_symm_single, LinearMap.BilinForm.dualBasis_injective, PiTensorProduct.dualDistribInvOfBasis_apply, NumberField.discr_eq_discr, Basis.restrictScalars_repr_apply, IsCyclotomicExtension.Rat.discr_prime_pow_ne_two', NumberField.Units.regOfFamily_of_isMaxRank, Basis.injective, FiniteDimensional.range_basisSingleton, Basis.coe_singleton, ZSpan.coe_floor_self, InnerProductSpace.coe_gramSchmidtBasis, linearMap_toMatrix_mul_basis_toMatrix, Basis.coe_reindex, instIsZLatticeRealSpan, LinearMap.toMatrix_transpose_apply, toMatrix_dualTensorHom, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, IsCyclotomicExtension.discr_prime_pow_ne_two, Basis.restrictScalars_apply, Basis.flag_succ, InnerProductSpace.gramSchmidt_triangular, Basis.mem_submodule_iff', Submodule.smithNormalFormBotBasis_def, Basis.sum_dual_apply_smul_coord, LinearMap.toMatrix_smulBasis_right, Basis.toDual_eq_repr, Basis.baseChange_end, Basis.sum_repr_mul_repr, LinearMap.BilinForm.dualBasis_eq_iff, Basis.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, Basis.mem_span_image, Basis.dualBasis_apply, Ideal.basisSpanSingleton_apply, Basis.sum_toMatrix_smul_self, PowerBasis.basis_eq_pow, ZSpan.span_top, Basis.reindexFinsetRange_repr_self, Algebra.discr_mul_isIntegral_mem_adjoin, LinearMap.detAux_def', LinearMap.toMatrix_transpose_apply', Basis.repr_symm_single_one, NumberField.mixedEmbedding.span_latticeBasis, Basis.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, exists_basis_of_span_of_maximalIdeal_rTensor_injective, Basis.multilinearMap_apply_apply, BilinForm.toMatrix_mul_basis_toMatrix, SymmetricAlgebra.equivMvPolynomial_symm_X, Basis.coe_parallelepiped, PeriodPair.latticeBasis_one, ZLattice.covolume_eq_det_mul_measureReal, ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite, ZSpan.isAddFundamentalDomain, Algebra.toMatrix_lmul', Basis.coe_ofVectorSpace, Basis.map_apply, Field.Emb.Cardinal.filtration_apply, Matrix.toLin_apply, Basis.smul_eq_map, Basis.coe_mk, Submodule.exists_smith_normal_form_of_rank_eq, Basis.smulTower'_apply, Basis.mem_ideal_iff', Polynomial.coe_basisMonomials, Finsupp.coe_basisSingleOne, Basis.sumCoords_self_apply, SymmetricAlgebra.equivMvPolynomial_ι_apply, Basis.repr_injective, Algebra.discr_powerBasis_eq_prod, Ideal.constr_basisSpanSingleton, Matrix.IsHermitian.eigenvectorUnitary_coe, Algebra.traceMatrix_of_basis, Field.Emb.Cardinal.deg_lt_aleph0, LinearMap.BilinForm.dualBasis_involutive, Basis.traceDual_involutive, TensorProduct.eq_repr_basis_left, Free.exists_set, Basis.end_repr_symm_apply, Basis.range_ofSpan, Basis.toMatrix_mul_toMatrix_flip, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, Basis.apply_eq_iff, LinearMap.eq_adjoint_iff_basis, Matrix.stdBasis_eq_single, Basis.det_self, Algebra.Generators.disjoint_ker_toKaehler_of_linearIndependent, OrthonormalBasis.orthonormal_adjustToOrientation, LinearMap.BilinForm.toMatrix_mul_basis_toMatrix, Matrix.toLinAlgEquiv_apply, Basis.coe_ofRepr, Basis.linearIndependent, Basis.self_mem_flag_iff, Basis.det_basis, Basis.mapCoeffs_apply, Algebra.SubmersivePresentation.basisCotangent_localizationAway_apply, Basis.det_inv, Basis.self_mem_span_image, Algebra.Generators.repr_CotangentSpaceMap, Basis.dualBasis_repr, TensorProduct.dualDistribInvOfBasis_apply, Basis.smulTower_apply, Basis.linearCombination_repr, Field.Emb.Cardinal.strictMono_filtration, BilinForm.toMatrix_apply, Basis.linearCombination_coord, Basis.toDual_apply, Algebra.Generators.toKaehler_cotangentSpaceBasis, ZSpan.quotientEquiv.symm_apply, NumberField.mem_span_integralBasis, RootPairing.Base.toWeightBasis_apply, Basis.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, Free.exists_basis, Pi.basisFun_apply, Matrix.toLinAlgEquiv_self, NumberField.mem_span_basisOfFractionalIdeal, Basis.coe_toDual_self, LinearMap.toMatrix₂_mul_basis_toMatrix, Basis.mem_ideal_iff, IsBaseChange.basis_apply, ZSpan.instDiscreteTopologySubtypeMemAddSubgroupToAddSubgroupIntSpanRangeCoeBasisRealOfFinite, NumberField.mixedEmbedding.latticeBasis_apply, Basis.sumQuot_inr, Basis.flag_le_iff, Subalgebra.LinearDisjoint.basisOfBasisLeft_apply, AddMonoidAlgebra.basis_apply, IsLocalRing.basisQuotient_apply, Orientation.coe_basisRightAngleRotation, free_def, Basis.localizationLocalization_span, Algebra.discr_localizationLocalization, Submodule.basisOfPid_bot, Basis.linearMap_apply_apply, Basis.toMatrix_isUnitSMul, coe_finsetBasisOfLinearIndependentOfCardEqFinrank, LinearMap.toMatrix₂_apply, Basis.ofVectorSpace_apply_self, Basis.algebraMapCoeffs_apply, WeierstrassCurve.Affine.CoordinateRing.basis_zero, Field.Emb.Cardinal.iSup_adjoin_eq_top, Basis.repr_sum_self, Basis.toMatrix_smul_left, Basis.self_mem_flag, LinearMap.BilinForm.dualSubmodule_flip_dualSubmodule_of_basis, AlternatingMap.measure_def, Basis.linearMap_repr_symm_apply, Basis.constr_basis, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, Basis.adjustToOrientation_apply_eq_or_eq_neg, Basis.finTwoProd_zero, FractionalIdeal.abs_det_basis_change, Basis.det_mul_det, Basis.toDual_linearCombination_right, Matrix.toLinearMapₛₗ₂_apply_basis, FiniteDimensional.exists_is_basis_integral, LinearMap.toMatrix_toSpanSingleton, Polynomial.degreeLT.addLinearEquiv_natAdd, Basis.singleton_apply, TensorProduct.equivFinsuppOfBasisRight_symm, Field.Emb.Cardinal.adjoin_image_leastExt, exteriorPower.basis_repr, Basis.exists_basis, Algebra.discr_powerBasis_eq_prod'', Algebra.traceMatrix_of_basis_mulVec, Basis.multilinearMap_apply, Field.Emb.Cardinal.instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, ZSpan.discreteTopology_pi_basisFun, Basis.traceDual_repr_apply, Basis.range_reindex, Polynomial.degreeLT.addLinearEquiv_symm_apply_inl_basis, LinearMap.coe_det, Basis.prod_apply_inl_fst, NumberField.basisOfFractionalIdeal_apply, nonempty_basis_of_flat_of_finrank_eq, Basis.ofSpan_apply_self, Basis.extendLe_apply_self, basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix, Algebra.discr_powerBasis_eq_prod', Basis.smul_apply, tendsto_card_div_pow_atTop_volume', Algebra.IsStandardSmooth.iff_exists_basis_kaehlerDifferential, Basis.tensorProduct_apply', LinearMap.eq_adjoint_iff_basis_right, Basis.ofIsLocalizedModule_span, LinearMap.toMatrixAlgEquiv_apply', Basis.equivFun_symm_single, AddSubgroup.relIndex_eq_natAbs_det, LinearMap.isSymm_iff_basis, Basis.constr_self, ZSpan.vadd_mem_fundamentalDomain, exteriorPower.ιMultiDual_apply_nondiag, Basis.traceDual_powerBasis_eq, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, ZSpan.fract_apply, Basis.toDual_apply_left, AddChar.coe_complexBasis, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, Matrix.toLinearMap₂_apply_basis, Basis.coe_mkFinCons, Basis.extendOfIsLattice_apply, IsCyclotomicExtension.Rat.discr_odd_prime', Basis.span_eq, Polynomial.degreeLT.basisProd_natAdd, Basis.det_unitsSMul_self, Basis.toDual_apply_right, NumberField.coe_discr, ZSpan.repr_floor_apply, Basis.repr_symm_apply, basis_toMatrix_mul_linearMap_toMatrix, exteriorPower.ιMulti_family_linearIndependent_ofBasis, Basis.coe_ofEquivFun, DualBases.coe_basis, LinearMap.toMatrixAlgEquiv_reindexRange, NumberField.mixedEmbedding.disjoint_span_commMap_ker, Basis.sum_equivFun, Field.Emb.Cardinal.adjoin_basis_eq_top, AddChar.complexBasis_apply, ZSpan.fract_eq_fract, Basis.ofIsCoprimeDifferentIdeal_apply, Complex.coe_basisOneI, Polynomial.Sequence.basis_degree_strictMono, Basis.sumQuot_inl, ZLattice.sum_piFinset_Icc_rpow_le, exists_basis_of_basis_baseChange, Algebra.SubmersivePresentation.basisCotangent_apply, Basis.coe_extend, Basis.repr_eq_iff', Basis.mk_eq_spanRank, LinearMap.BilinForm.isSymm_iff_basis, Basis.toMatrix_self, PeriodPair.lattice_eq_span_range_basis, basis_toMatrix_mul, Ideal.natAbs_det_basis_change, Basis.unitsSMul_apply, Basis.mem_span_repr_support, Basis.toMatrix_mul_toMatrix, Algebra.leftMulMatrix_eq_repr_mul, Basis.toDual_eq_equivFun, Polynomial.degreeLT.basisProd_castAdd, Basis.sum_repr, Basis.toMatrix_mulVec_repr, Algebra.Generators.basisCotangentAway_apply, TensorProduct.sum_tmul_basis_left_injective, Submodule.basis_of_pid_aux, TensorProduct.equivFinsuppOfBasisRight_symm_apply, Basis.toMatrix_unitsSMul, Basis.prod_apply_inr_snd, Basis.mem_span_iff_repr_mem, hasEigenvector_toLin_diagonal, Basis.addHaar_self, Basis.toMatrix_map_vecMul, LinearMap.toMatrixAlgEquiv_transpose_apply, Basis.repr_self, QuadraticMap.basisRepr_apply, Basis.piTensorProduct_apply, WeierstrassCurve.Affine.CoordinateRing.basis_apply, ZSpan.setFinite_inter, Basis.reindex_apply, Submodule.exists_smith_normal_form_of_le, LinearMap.toMatrix_apply, Basis.instSMulCommClass, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, Basis.restrictScalars_toMatrix, FinitePresentation.exists_basis_localizedModule_powers, LinearMap.toMatrix_id_eq_basis_toMatrix, LinearMap.toMatrixAlgEquiv_transpose_apply', Basis.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', Basis.traceDual_injective, Basis.baseChange_linearMap, IsCyclotomicExtension.discr_prime_pow, ZSpan.fundamentalDomain_ae_parallelepiped, Basis.groupSMul_apply, BoxIntegral.unitPartition.tag_mem_smul_span, LinearMap.BilinForm.apply_dualBasis_right, ZLattice.covolume_eq_det, LinearMap.sum_repr_mul_repr_mul, Basis.coe_ofSpan, IsAdjoinRootMonic.basis_one, IsCyclotomicExtension.discr_prime_pow_ne_two', Submodule.natAbs_det_basis_change, Submodule.nonempty_basis_of_pid, Basis.traceDual_eq_iff, Algebra.discr_reindex, Trivialization.localFrame_apply_of_mem_baseSet, IsAdjoinRootMonic.basis_apply, AffineBasis.basisOf_apply, TensorProduct.eq_repr_basis_right
|