| Name | Category | Theorems |
|---|
cons_val ๐ | CompOp | โ |
matchVecConsPrefix ๐ | CompOp | โ |
vecAlt0 ๐ | CompOp | 5 mathmath: cons_vec_bit0_eq_alt0, vecHead_vecAlt0, empty_vecAlt0, cons_vecAlt0, vecAlt0_vecAppend
|
vecAlt1 ๐ | CompOp | 5 mathmath: cons_vecAlt1, cons_vec_bit1_eq_alt1, vecHead_vecAlt1, empty_vecAlt1, vecAlt1_vecAppend
|
vecAppend ๐ | CompOp | 9 mathmath: cons_vec_bit1_eq_alt1, cons_vecAppend, empty_vecAppend, vecAppend_empty, cons_vec_bit0_eq_alt0, vecAlt1_vecAppend, vecAlt0_vecAppend, vecAppend_apply_zero, vecAppend_eq_ite
|
vecCons ๐ | CompOp | 393 mathmath: affineIndependent_of_ne_of_notMem_of_mem_of_mem, WeierstrassCurve.Jacobian.addXYZ_of_Z_ne_zero, range_cons, Orientation.oangle_ne_zero_and_ne_pi_iff_linearIndependent, replicateCol_cons, WeierstrassCurve.Jacobian.addXYZ_self, SSet.stdSimplex.coe_triangle_down_toOrderHom, Projectivization.dependent_pair_iff_eq, cons_vecAlt1, List.Nat.antidiagonalTuple_two, EuclideanGeometry.side_angle_side, LinearIndependent.pair_iff, CompleteOrthogonalIdempotents.pair_iff, LinearIndependent.pair_add_smul_right_iff, vec2_eq, AlternatingMap.map_vecCons_smul, LinearIndependent.pair_add_smul_left_iff, Homeomorph.finTwoArrow_symm_apply, WeierstrassCurve.Jacobian.add_of_Y_ne', FirstOrder.Language.Formula.realize_relโ, adjugate_fin_two, diagonal_vec3, EuclideanGeometry.Cospherical.affineIndependent_of_mem_of_ne, Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat_left, affineIndependent_iff_not_collinear_set, WeierstrassCurve.Projective.negY_eq, affineIndependent_of_ne_of_mem_of_notMem_of_mem, cons_fin_one, WeierstrassCurve.Projective.nonsingularLift_some, CartanMatrix.C_two, stdSimplexHomeomorphUnitInterval_symm_apply_coe, SSet.Truncated.Path.mkโ_arrow, Function.fromTypes_cons_equiv_symm_apply, ContinuousAlternatingMap.vecCons_smul, RootPairing.linearIndependent_of_sub_mem_range_root', submatrix_cons_row, diagonal_fin_two, bilinearIteratedFDerivTwo_eq_iteratedFDeriv, WeierstrassCurve.Projective.equiv_some_of_Z_ne_zero, Multiset.Nat.antidiagonalTuple_one, ContinuousOn.matrixVecCons, ContinuousAlternatingMap.map_insertNth, strictAnti_vecEmpty, CartanMatrix.D_four, EisensteinSeries.abs_le_right_of_norm, sub_cons, WittVector.zsmul_coeff, sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent, neg_cons, add_cons, List.Nat.antidiagonalTuple_one, WeierstrassCurve.Affine.CoordinateRing.coe_basis, RootPairing.coxeterWeightIn_eq_four_iff_not_linearIndependent, WittVector.pow_coeff, WeierstrassCurve.Jacobian.negY_eq, diagonal_vec1, WeierstrassCurve.Jacobian.addXYZ_of_X_eq, Finset.Nat.antidiagonalTuple_one, cons_val_succ', WeierstrassCurve.Projective.add_of_Z_eq_zero, RootPairing.Base.linearIndependent_pair_of_ne, WeierstrassCurve.Projective.Point.zero_point, tensorIteratedFDerivTwo_eq_iteratedFDeriv, QuadraticAlgebra.linearEquivTuple_apply, Complex.coe_orthonormalBasisOneI, Function.FromTypes.uncurry_apply_cons, Complex.measurableEquivPi_apply, EisensteinSeries.e2Summand_summable, cons_vec_bit1_eq_alt1, FirstOrder.Language.Relations.realize_irreflexive, MeasureTheory.measurePreserving_finTwoArrow_vec, WeierstrassCurve.Jacobian.Point.fromAffine_some, WeierstrassCurve.Jacobian.add_of_Y_eq, Orientation.areaForm_to_volumeForm, Multiset.Nat.antidiagonalTuple_two, cons_val_two, Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_right, LinearIndependent.pair_iffโ, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_complexPlane, head_cons, tail_cons, diagonal_vec2, RootPairing.IsReduced.linearIndependent_iff, FirstOrder.Language.Formula.realize_relโ, GeneralLinearGroup.upperRightHom_apply, monotone_vecEmpty, WeierstrassCurve.Jacobian.smul_fin3, ContinuousLinearEquiv.finTwoArrow_symm_apply, Monotone.vecCons, cons_val_one, Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat_right, tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin, WeierstrassCurve.Projective.addXYZ_of_X_eq, ModularGroup.lcRow0Extend_symm_apply, vec3_add, strictMono_vecEmpty, ContinuousAlternatingMap.curryLeft_apply_apply, WeierstrassCurve.Jacobian.negMap_of_Z_ne_zero, WeierstrassCurve.Jacobian.equiv_zero_of_Z_eq_zero, LinearIndependent.pair_neg_left_iff, RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four, adjugate_fin_three, natCast_fin_three, CartanMatrix.D_three, Polynomial.aeval_homogenize_X_one, vec3_eq, Fin.sum_univ_two', eta_fin_three, cons_val_zero, Height.logHeightโ_div_eq_logHeight, extDeriv_apply_vectorField, Complex.orthonormalBasisOneI_repr_apply, exists_linearIndependent_pair_of_one_lt_rank, replicateRow_cons, LinearIndependent.pair_smul_iff, AlternatingMap.curryLeft_apply_apply, Nat.multinomial_univ_two, injective_pair_iff_ne, EuclideanGeometry.Cospherical.affineIndependent_of_ne, FirstOrder.Language.Relations.realize_transitive, natCast_fin_two, cons_dotProduct, WeierstrassCurve.Jacobian.fin3_def, eta_fin_two, Height.mulHeight_swap, Continuous.matrixVecCons, WeierstrassCurve.Jacobian.dblXYZ_of_Z_ne_zero, StrictMono.vecCons, WeierstrassCurve.Jacobian.negMap_of_Z_eq_zero, Fin.tail_vecCons, LinearMap.BilinForm.apply_mul_apply_lt_iff_linearIndependent, ModularGroup.lcRow0Extend_apply, LinearMap.vecCons_apply, WittVector.IsPolyโ.poly, ModularGroup.coe_T_inv, Function.fromTypes_cons, RootPairing.EmbeddedG2.allRoots_eq_map_allCoeffs, RootPairing.EmbeddedG2.linearIndependent_short_long, CartanMatrix.B_two, exists_linearIndependent_pair_of_one_lt_finrank, WeierstrassCurve.Jacobian.nonsingularLift_some, cons_val_succ, adjugate_fin_three_of, WeierstrassCurve.Projective.addXYZ_neg, RootPairing.chainTopCoeff_eq_zero_iff, ofNat_fin_three, LinearMap.BilinForm.apply_sq_lt_iff_linearIndependent_of_symm, cons_val_fin_one, SSet.stdSimplex.coe_edge_down_toOrderHom, finTwoArrowEquiv_symm_apply, ofNat_fin_two, WeierstrassCurve.Jacobian.addMap_of_Z_ne_zero, similar_of_side_side, RootPairing.linearIndependent_of_add_mem_range_root, WeierstrassCurve.Projective.addXYZ_of_Z_ne_zero, cons_add_cons, RootPairing.linearIndependent_of_add_mem_range_root', cons_transpose, FirstOrder.Language.BoundedFormula.realize_relโ, ContinuousAt.matrixVecCons, antitone_vecCons, iteratedDeriv_vcomp_three, vec3_dotProduct', iteratedFDerivWithin_two_apply', Quaternion.equivTuple_apply, QuadraticAlgebra.basis_repr_apply, toLin_finTwoProd_apply, diagonal_fin_one, RootPairing.linearIndependent_iff_coxeterWeight_ne_four, val_planeConformalMatrix, UniformEquiv.finTwoArrow_symm_apply, cons_mul, WeierstrassCurve.Jacobian.addXYZ_neg, Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_left, RootPairing.IsReduced.linearIndependent, EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent, WeierstrassCurve.Projective.dblXYZ_of_Z_eq_zero, Complex.coe_basisOneI_repr, Finsupp.ofSupportFinite_fin_two_eq, WeierstrassCurve.Projective.Point.fromAffine_some, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis, vecCons_const, SpecialLinearGroup.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero, WeierstrassCurve.Projective.negMap_of_Z_ne_zero, cross_apply, WeierstrassCurve.Projective.smul_fin3, FirstOrder.Language.Relations.realize_total, SpecialLinearGroup.SL2_inv_expl, CartanMatrix.A_three, WeierstrassCurve.Projective.neg_of_Z_ne_zero, smul_vec3, LinearIndependent.pair_symm_iff, Module.Basis.coe_finTwoProd_repr, extDerivWithin_apply_vectorField, trace_fin_one_of, liftFun_vecCons, EuclideanGeometry.similar_of_side_angle_side, affineIndependent_of_ne, WeierstrassCurve.Jacobian.nonsingularLift_zero, Algebra.leftMulMatrix_complex, vecCons_inj, LinearEquiv.finTwoArrow_symm_apply, WittVector.sub_coeff, Projectivization.independent_pair_iff_ne, WittVector.mul_coeff, WeierstrassCurve.Projective.dblXYZ_of_Z_ne_zero, WeierstrassCurve.Projective.comp_fin3, WeierstrassCurve.Projective.addMap_of_Y_eq, cons_sub, Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis, WeierstrassCurve.Projective.fin3_def, Fin.prod_univ_two', QuaternionAlgebra.equivTuple_apply, EisensteinSeries.norm_symm, LinearIndependent.pair_iff', ContinuousAlternatingMap.vecCons_add, AlternatingMap.map_vecCons_add, vec2_add, affineIndependent_iff_affineIndependent_collinear_ne, cons_zero_zero, SSet.horn.edgeโ_coe_down, cons_eq_zero_iff, WeierstrassCurve.Projective.fin3_def_ext, Orientation.rotation_eq_matrix_toLin, IsSymmSndFDerivAt.iteratedFDeriv_cons, cons_sub_cons, CartanMatrix.A_two, CartanMatrix.D_two, StrictAnti.vecCons, WeierstrassCurve.Jacobian.fin3_def_ext, cons_vecAppend, Height.mulHeightโ_eq_mulHeight, WeierstrassCurve.Jacobian.dblXYZ_of_Y_eq', InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, finTwoArrowEquiv'_symm_apply, WeierstrassCurve.Jacobian.add_of_X_ne, vec2_dotProduct', Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat, triple_product_eq_det, InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane, bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv, EuclideanGeometry.similar_of_angle_angle, ContinuousAlternatingMap.map_vecCons_sub, vec_single_eq_const, WeierstrassCurve.Projective.add_of_Y_eq, of_mem_specialOrthogonalGroup_fin_two_iff, cons_head_tail, ContinuousWithinAt.matrixVecCons, range_cons_cons_empty, WeierstrassCurve.Projective.add_of_X_ne, SpecialLinearGroup.SL2_inv_expl_det, crossProduct_ne_zero_iff_linearIndependent, smul_cons, sameRay_or_sameRay_neg_iff_not_linearIndependent, FirstOrder.Language.Relations.realize_symmetric, WeierstrassCurve.Projective.Point.zero_def, QuaternionAlgebra.coe_basisOneIJK_repr, WeierstrassCurve.Projective.add_of_Y_ne', WeierstrassCurve.Projective.neg_of_Z_eq_zero, Height.logHeightโ_eq_logHeight, CompleteOrthogonalIdempotents.of_isIdempotentElem, Orientation.coe_basisRightAngleRotation, one_fin_three, toLin_finTwoProd_toContinuousLinearMap, LinearIndependent.pair_add_left_iff, WittVector.v2_coeff, WeierstrassCurve.Jacobian.dblXYZ_of_Z_eq_zero, smul_mat_cons, RootPairing.coxeterWeight_eq_four_iff_not_linearIndependent, WeierstrassCurve.Projective.negMap_of_Z_eq_zero, WeierstrassCurve.Jacobian.nonsingular_some, CompleteOrthogonalIdempotents.pair_iff'โ, cons_val_zero', trace_fin_three_of, WeierstrassCurve.Projective.addMap_of_Z_ne_zero, WeierstrassCurve.Projective.equiv_zero_of_Z_eq_zero, EuclideanGeometry.angle_side_angle, cons_add, summable_prod_eisSummand, EisensteinSeries.abs_le_left_of_norm, toLin_finTwoProd, cons_vec_bit0_eq_alt0, collinear_iff_not_affineIndependent_set, EuclideanGeometry.angle_angle_side, EuclideanGeometry.side_side_side, mul_fin_two, EisensteinSeries.abs_norm_eq_max_natAbs, WeierstrassCurve.Projective.nonsingular_some, InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis, FirstOrder.Language.simpleGraphOfStructure_adj, Complex.toMatrix_conjAe, cons_vecMulVec, cons_vecMul, det_fin_one_of, UpperHalfPlane.val_J, WeierstrassCurve.Jacobian.Point.zero_point, vecMulVec_cons, ModularGroup.coe_T, WeierstrassCurve.Jacobian.Point.toAffine_zero, LinearIndependent.pair_neg_right_iff, cons_vecMul_cons, dotProduct_cons, strictMono_vecCons, algebraicIndependent_iff_transcendental, det_fin_two_of, similar_of_dist_mul_eq_dist_mul_eq, WeierstrassCurve.Jacobian.equation_zero, EisensteinSeries.abs_norm_eq_max_natAbs_neg, range_cons_empty, WeierstrassCurve.Projective.nonsingular_zero, WeierstrassCurve.Jacobian.Point.zero_def, SSet.Truncated.Path.mkโ_vertex, Height.mulHeightโ_div_eq_mulHeight, cons_mulVec, mul_fin_three, WittVector.neg_coeff, SSet.horn.primitiveEdge_coe_down, WeierstrassCurve.Jacobian.equation_some, affineIndependent_of_ne_of_mem_of_mem_of_notMem, AlternatingMap.neg_one_pow_smul_map_insertNth, Antitone.vecCons, WeierstrassCurve.Projective.Point.toAffine_zero, stdSimplexEquivIcc_symm_apply_coe, WeierstrassCurve.Jacobian.neg_of_Z_ne_zero, Filter.Tendsto.matrixVecCons, AlternatingMap.map_insertNth, CartanMatrix.A_one, ContinuousAlternatingMap.neg_one_pow_smul_map_insertNth, FirstOrder.Language.Theory.simpleGraph_model_iff, Fin.preimage_apply_01_prod', smul_vec2, RootPairing.chainBotCoeff_eq_zero_iff, cons_val_four, LinearMap.BilinForm.not_linearIndependent_of_apply_mul_apply_eq, WeierstrassCurve.Jacobian.nonsingular_zero, WittVector.peval_polyOfInterest', StandardEtalePresentation.toPresentation_relation, Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat, ModularGroup.coe_T_zpow, PeriodPair.indep, diagonal_fin_three, Quaternion.linearIsometryEquivTuple_apply, Function.fromTypes_cons_equiv_apply, strictAnti_vecCons, WeierstrassCurve.Projective.add_of_Y_ne, const_fin1_eq, cons_vecAlt0, EuclideanGeometry.affineIndependent_iff_of_two_zsmul_oangle_eq, WeierstrassCurve.Projective.equation_zero, WeierstrassCurve.Jacobian.equiv_some_of_Z_ne_zero, ModularGroup.coe_S, vecMul_cons, Complex.coe_basisOneI, WeierstrassCurve.Jacobian.dblXYZ_of_Y_eq, FirstOrder.Language.Relations.realize_reflexive, WittVector.add_coeff, mulVec_cons, orthonormal_vecCons_iff, WeierstrassCurve.Jacobian.add_of_Z_eq_zero, cons_val_three, WeierstrassCurve.Jacobian.comp_fin3, antitone_vecEmpty, monotone_vecCons, WeierstrassCurve.Projective.equation_some, RootPairing.linearIndependent_of_sub_mem_range_root, WeierstrassCurve.Jacobian.addMap_of_Y_eq, EisensteinSeries.vec_add_const_isTheta, cons_dotProduct_cons, WeierstrassCurve.Projective.dblXYZ_of_Y_eq, WeierstrassCurve.Projective.nonsingularLift_zero, ExteriorAlgebra.liftAlternating_ฮน, adjugate_fin_two_of, one_fin_two, Nat.multinomial_univ_three, LinearIndependent.pair_add_smul_add_smul_iff, WeierstrassCurve.Jacobian.neg_of_Z_eq_zero, FirstOrder.Language.Term.realize_functions_applyโ, trace_fin_two_of, FirstOrder.Language.Relations.realize_antisymmetric, CompleteOrthogonalIdempotents.pair_iffโ, LinearIndependent.pair_add_right_iff, Function.FromTypes.curry_apply_cons, FirstOrder.Language.BoundedFormula.realize_relโ, WittVector.nsmul_coeff, IsSymmSndFDerivWithinAt.iteratedFDerivWithin_cons, WeierstrassCurve.Projective.addXYZ_self, WeierstrassCurve.Jacobian.add_of_Y_ne, WittVector.peval_polyOfInterest, cons_val', iteratedDerivWithin_vcomp_three, FirstOrder.Language.Term.realize_functions_applyโ, WeierstrassCurve.Jacobian.neg_of_Z_eq_zero'
|
vecConsUnexpander ๐ | CompOp | โ |
vecEmpty ๐ | CompOp | 341 mathmath: replicateCol_empty, affineIndependent_of_ne_of_notMem_of_mem_of_mem, WeierstrassCurve.Jacobian.addXYZ_of_Z_ne_zero, Orientation.oangle_ne_zero_and_ne_pi_iff_linearIndependent, vecMulVec_empty, WeierstrassCurve.Jacobian.addXYZ_self, SSet.stdSimplex.coe_triangle_down_toOrderHom, empty_mulVec, Projectivization.dependent_pair_iff_eq, List.Nat.antidiagonalTuple_two, EuclideanGeometry.side_angle_side, LinearIndependent.pair_iff, CompleteOrthogonalIdempotents.pair_iff, LinearIndependent.pair_add_smul_right_iff, vec2_eq, LinearIndependent.pair_add_smul_left_iff, Homeomorph.finTwoArrow_symm_apply, WeierstrassCurve.Jacobian.add_of_Y_ne', FirstOrder.Language.Formula.realize_relโ, adjugate_fin_two, diagonal_vec3, EuclideanGeometry.Cospherical.affineIndependent_of_mem_of_ne, Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat_left, affineIndependent_iff_not_collinear_set, List.Nat.antidiagonalTuple_zero_zero, WeierstrassCurve.Projective.negY_eq, affineIndependent_of_ne_of_mem_of_notMem_of_mem, WeierstrassCurve.Projective.nonsingularLift_some, CartanMatrix.C_two, stdSimplexHomeomorphUnitInterval_symm_apply_coe, SSet.Truncated.Path.mkโ_arrow, RootPairing.linearIndependent_of_sub_mem_range_root', diagonal_fin_two, bilinearIteratedFDerivTwo_eq_iteratedFDeriv, WeierstrassCurve.Projective.equiv_some_of_Z_ne_zero, Multiset.Nat.antidiagonalTuple_one, strictAnti_vecEmpty, CartanMatrix.D_four, EisensteinSeries.abs_le_right_of_norm, WittVector.zsmul_coeff, sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent, List.Nat.antidiagonalTuple_one, WeierstrassCurve.Affine.CoordinateRing.coe_basis, RootPairing.coxeterWeightIn_eq_four_iff_not_linearIndependent, WittVector.pow_coeff, WeierstrassCurve.Jacobian.negY_eq, diagonal_vec1, WeierstrassCurve.Jacobian.addXYZ_of_X_eq, Finset.Nat.antidiagonalTuple_one, WeierstrassCurve.Projective.add_of_Z_eq_zero, RootPairing.Base.linearIndependent_pair_of_ne, WeierstrassCurve.Projective.Point.zero_point, tensorIteratedFDerivTwo_eq_iteratedFDeriv, QuadraticAlgebra.linearEquivTuple_apply, Complex.coe_orthonormalBasisOneI, smul_empty, Complex.measurableEquivPi_apply, EisensteinSeries.e2Summand_summable, FirstOrder.Language.Relations.realize_irreflexive, MeasureTheory.measurePreserving_finTwoArrow_vec, WeierstrassCurve.Jacobian.Point.fromAffine_some, WeierstrassCurve.Jacobian.add_of_Y_eq, Orientation.areaForm_to_volumeForm, Multiset.Nat.antidiagonalTuple_two, Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_right, LinearIndependent.pair_iffโ, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_complexPlane, diagonal_vec2, RootPairing.IsReduced.linearIndependent_iff, FirstOrder.Language.Formula.realize_relโ, GeneralLinearGroup.upperRightHom_apply, monotone_vecEmpty, WeierstrassCurve.Jacobian.smul_fin3, ContinuousLinearEquiv.finTwoArrow_symm_apply, Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat_right, tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin, WeierstrassCurve.Projective.addXYZ_of_X_eq, ModularGroup.lcRow0Extend_symm_apply, vec3_add, empty_sub_empty, strictMono_vecEmpty, WeierstrassCurve.Jacobian.negMap_of_Z_ne_zero, WeierstrassCurve.Jacobian.equiv_zero_of_Z_eq_zero, LinearIndependent.pair_neg_left_iff, RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four, submatrix_empty, adjugate_fin_three, natCast_fin_three, CartanMatrix.D_three, Polynomial.aeval_homogenize_X_one, vec3_eq, Fin.sum_univ_two', eta_fin_three, replicateRow_empty, Height.logHeightโ_div_eq_logHeight, Complex.orthonormalBasisOneI_repr_apply, exists_linearIndependent_pair_of_one_lt_rank, LinearIndependent.pair_smul_iff, Nat.multinomial_univ_two, Function.fromTypes_nil_equiv_apply, injective_pair_iff_ne, EuclideanGeometry.Cospherical.affineIndependent_of_ne, FirstOrder.Language.Relations.realize_transitive, natCast_fin_two, WeierstrassCurve.Jacobian.fin3_def, Finset.Nat.antidiagonalTuple_zero_zero, eta_fin_two, Height.mulHeight_swap, WeierstrassCurve.Jacobian.dblXYZ_of_Z_ne_zero, transpose_empty_cols, WeierstrassCurve.Jacobian.negMap_of_Z_eq_zero, LinearMap.BilinForm.apply_mul_apply_lt_iff_linearIndependent, ModularGroup.lcRow0Extend_apply, empty_val', WittVector.IsPolyโ.poly, ModularGroup.coe_T_inv, RootPairing.EmbeddedG2.allRoots_eq_map_allCoeffs, RootPairing.EmbeddedG2.linearIndependent_short_long, CartanMatrix.B_two, exists_linearIndependent_pair_of_one_lt_finrank, WeierstrassCurve.Jacobian.nonsingularLift_some, adjugate_fin_three_of, WeierstrassCurve.Projective.addXYZ_neg, RootPairing.chainTopCoeff_eq_zero_iff, ofNat_fin_three, LinearMap.BilinForm.apply_sq_lt_iff_linearIndependent_of_symm, SSet.stdSimplex.coe_edge_down_toOrderHom, WittVector.matrix_vecEmpty_coeff, empty_add_empty, finTwoArrowEquiv_symm_apply, ofNat_fin_two, WeierstrassCurve.Jacobian.addMap_of_Z_ne_zero, similar_of_side_side, RootPairing.linearIndependent_of_add_mem_range_root, WeierstrassCurve.Projective.addXYZ_of_Z_ne_zero, RootPairing.linearIndependent_of_add_mem_range_root', FirstOrder.Language.BoundedFormula.realize_relโ, iteratedDeriv_vcomp_three, vec3_dotProduct', iteratedFDerivWithin_two_apply', Quaternion.equivTuple_apply, QuadraticAlgebra.basis_repr_apply, toLin_finTwoProd_apply, diagonal_fin_one, RootPairing.linearIndependent_iff_coxeterWeight_ne_four, val_planeConformalMatrix, UniformEquiv.finTwoArrow_symm_apply, WeierstrassCurve.Jacobian.addXYZ_neg, Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_left, RootPairing.IsReduced.linearIndependent, EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent, WeierstrassCurve.Projective.dblXYZ_of_Z_eq_zero, Complex.coe_basisOneI_repr, Finsupp.ofSupportFinite_fin_two_eq, WeierstrassCurve.Projective.Point.fromAffine_some, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis, SpecialLinearGroup.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero, WeierstrassCurve.Projective.negMap_of_Z_ne_zero, cross_apply, WeierstrassCurve.Projective.smul_fin3, FirstOrder.Language.Relations.realize_total, SpecialLinearGroup.SL2_inv_expl, CartanMatrix.A_three, WeierstrassCurve.Projective.neg_of_Z_ne_zero, smul_vec3, LinearIndependent.pair_symm_iff, Module.Basis.coe_finTwoProd_repr, trace_fin_one_of, EuclideanGeometry.similar_of_side_angle_side, affineIndependent_of_ne, WeierstrassCurve.Jacobian.nonsingularLift_zero, Algebra.leftMulMatrix_complex, LinearEquiv.finTwoArrow_symm_apply, WittVector.sub_coeff, Projectivization.independent_pair_iff_ne, WittVector.mul_coeff, WeierstrassCurve.Projective.dblXYZ_of_Z_ne_zero, WeierstrassCurve.Projective.comp_fin3, WeierstrassCurve.Projective.addMap_of_Y_eq, Function.fromTypes_nil, Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis, WeierstrassCurve.Projective.fin3_def, Fin.prod_univ_two', QuaternionAlgebra.equivTuple_apply, EisensteinSeries.norm_symm, LinearIndependent.pair_iff', vec2_add, affineIndependent_iff_affineIndependent_collinear_ne, empty_eq, SSet.horn.edgeโ_coe_down, WeierstrassCurve.Projective.fin3_def_ext, Orientation.rotation_eq_matrix_toLin, IsSymmSndFDerivAt.iteratedFDeriv_cons, CartanMatrix.A_two, CartanMatrix.D_two, WeierstrassCurve.Jacobian.fin3_def_ext, Height.mulHeightโ_eq_mulHeight, WeierstrassCurve.Jacobian.dblXYZ_of_Y_eq', InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, finTwoArrowEquiv'_symm_apply, WeierstrassCurve.Jacobian.add_of_X_ne, vec2_dotProduct', Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat, Topology.RelCWComplex.openCell_zero_eq_singleton, triple_product_eq_det, InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane, bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv, EuclideanGeometry.similar_of_angle_angle, empty_vecAppend, LinearMap.vecEmpty_apply, mul_empty, vec_single_eq_const, WeierstrassCurve.Projective.add_of_Y_eq, of_mem_specialOrthogonalGroup_fin_two_iff, WeierstrassCurve.Projective.add_of_X_ne, SpecialLinearGroup.SL2_inv_expl_det, crossProduct_ne_zero_iff_linearIndependent, sameRay_or_sameRay_neg_iff_not_linearIndependent, FirstOrder.Language.Relations.realize_symmetric, WeierstrassCurve.Projective.Point.zero_def, vecAppend_empty, QuaternionAlgebra.coe_basisOneIJK_repr, WeierstrassCurve.Projective.add_of_Y_ne', WeierstrassCurve.Projective.neg_of_Z_eq_zero, Height.logHeightโ_eq_logHeight, CompleteOrthogonalIdempotents.of_isIdempotentElem, Orientation.coe_basisRightAngleRotation, one_fin_three, toLin_finTwoProd_toContinuousLinearMap, LinearIndependent.pair_add_left_iff, WittVector.v2_coeff, WeierstrassCurve.Jacobian.dblXYZ_of_Z_eq_zero, Topology.RelCWComplex.closedCell_zero_eq_singleton, RootPairing.coxeterWeight_eq_four_iff_not_linearIndependent, WeierstrassCurve.Projective.negMap_of_Z_eq_zero, WeierstrassCurve.Jacobian.nonsingular_some, CompleteOrthogonalIdempotents.pair_iff'โ, empty_mul, trace_fin_three_of, WeierstrassCurve.Projective.addMap_of_Z_ne_zero, WeierstrassCurve.Projective.equiv_zero_of_Z_eq_zero, EuclideanGeometry.angle_side_angle, summable_prod_eisSummand, EisensteinSeries.abs_le_left_of_norm, toLin_finTwoProd, collinear_iff_not_affineIndependent_set, EuclideanGeometry.angle_angle_side, EuclideanGeometry.side_side_side, mul_fin_two, empty_vecAlt1, EisensteinSeries.abs_norm_eq_max_natAbs, WeierstrassCurve.Projective.nonsingular_some, InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis, FirstOrder.Language.simpleGraphOfStructure_adj, Complex.toMatrix_conjAe, det_fin_one_of, UpperHalfPlane.val_J, WeierstrassCurve.Jacobian.Point.zero_point, ModularGroup.coe_T, WeierstrassCurve.Jacobian.Point.toAffine_zero, LinearIndependent.pair_neg_right_iff, algebraicIndependent_iff_transcendental, det_fin_two_of, similar_of_dist_mul_eq_dist_mul_eq, WeierstrassCurve.Jacobian.equation_zero, EisensteinSeries.abs_norm_eq_max_natAbs_neg, WeierstrassCurve.Projective.nonsingular_zero, WeierstrassCurve.Jacobian.Point.zero_def, SSet.Truncated.Path.mkโ_vertex, Height.mulHeightโ_div_eq_mulHeight, mul_fin_three, WittVector.neg_coeff, SSet.horn.primitiveEdge_coe_down, WeierstrassCurve.Jacobian.equation_some, affineIndependent_of_ne_of_mem_of_mem_of_notMem, WeierstrassCurve.Projective.Point.toAffine_zero, stdSimplexEquivIcc_symm_apply_coe, WeierstrassCurve.Jacobian.neg_of_Z_ne_zero, CartanMatrix.A_one, FirstOrder.Language.Theory.simpleGraph_model_iff, Fin.preimage_apply_01_prod', smul_vec2, RootPairing.chainBotCoeff_eq_zero_iff, LinearMap.BilinForm.not_linearIndependent_of_apply_mul_apply_eq, WeierstrassCurve.Jacobian.nonsingular_zero, WittVector.peval_polyOfInterest', StandardEtalePresentation.toPresentation_relation, empty_vecMulVec, Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat, ModularGroup.coe_T_zpow, PeriodPair.indep, diagonal_fin_three, Quaternion.linearIsometryEquivTuple_apply, neg_empty, transpose_empty_rows, empty_vecAlt0, WeierstrassCurve.Projective.add_of_Y_ne, const_fin1_eq, EuclideanGeometry.affineIndependent_iff_of_two_zsmul_oangle_eq, WeierstrassCurve.Projective.equation_zero, WeierstrassCurve.Jacobian.equiv_some_of_Z_ne_zero, ModularGroup.coe_S, Complex.coe_basisOneI, WeierstrassCurve.Jacobian.dblXYZ_of_Y_eq, FirstOrder.Language.Relations.realize_reflexive, WittVector.add_coeff, WeierstrassCurve.Jacobian.add_of_Z_eq_zero, WeierstrassCurve.Jacobian.comp_fin3, zero_empty, antitone_vecEmpty, WeierstrassCurve.Projective.equation_some, RootPairing.linearIndependent_of_sub_mem_range_root, WeierstrassCurve.Jacobian.addMap_of_Y_eq, EisensteinSeries.vec_add_const_isTheta, WeierstrassCurve.Projective.dblXYZ_of_Y_eq, Multiset.Nat.antidiagonalTuple_zero_zero, WeierstrassCurve.Projective.nonsingularLift_zero, ExteriorAlgebra.liftAlternating_ฮน, adjugate_fin_two_of, one_fin_two, Nat.multinomial_univ_three, LinearIndependent.pair_add_smul_add_smul_iff, WeierstrassCurve.Jacobian.neg_of_Z_eq_zero, FirstOrder.Language.Term.realize_functions_applyโ, trace_fin_two_of, FirstOrder.Language.Relations.realize_antisymmetric, CompleteOrthogonalIdempotents.pair_iffโ, LinearIndependent.pair_add_right_iff, FirstOrder.Language.BoundedFormula.realize_relโ, WittVector.nsmul_coeff, IsSymmSndFDerivWithinAt.iteratedFDerivWithin_cons, WeierstrassCurve.Projective.addXYZ_self, WeierstrassCurve.Jacobian.add_of_Y_ne, WittVector.peval_polyOfInterest, iteratedDerivWithin_vcomp_three, FirstOrder.Language.Term.realize_functions_applyโ, smul_mat_empty, vecMul_empty, WeierstrassCurve.Jacobian.neg_of_Z_eq_zero', Function.fromTypes_nil_equiv_symm_apply
|
vecEmptyUnexpander ๐ | CompOp | โ |
vecHead ๐ | CompOp | 25 mathmath: head_val', sub_cons, add_cons, cons_val_two, head_cons, head_fin_const, cons_dotProduct, Function.FromTypes.uncurry_two_eq_uncurry, cons_sub, vecHead_vecAlt1, cons_head_tail, Function.OfArity.uncurry_two_eq_uncurry, head_add, cons_add, head_sub, cons_vecMul, dotProduct_cons, vecHead_vecAlt0, cons_val_four, vecMul_cons, mulVec_cons, head_transpose, cons_val_three, head_zero, head_neg
|
vecNotation ๐ | CompOp | โ |
vecTail ๐ | CompOp | 27 mathmath: sub_cons, add_cons, mul_val_succ, ExteriorAlgebra.ฮนMulti_succ_apply, cons_val_two, tail_cons, cons_dotProduct, Function.FromTypes.const_succ_apply, tail_val', Function.FromTypes.uncurry_apply_succ, tail_add, tail_zero, Function.FromTypes.uncurry_two_eq_uncurry, Function.FromTypes.const_succ, cons_sub, cons_head_tail, tail_transpose, Function.OfArity.uncurry_two_eq_uncurry, cons_add, tail_sub, cons_vecMul, dotProduct_cons, cons_val_four, tail_neg, vecMul_cons, mulVec_cons, cons_val_three
|