All.lean
Nyll.AlgebraicCurves.Foundations.Polynomial.All
0 declarations indexed from sourceView source ↗
Imports27
- Nyll.AlgebraicCurves.Foundations.Polynomial.AddCommGroup_exists_mvPolynomial_totalDegree_le_eval_eq_of_forall_exists_polynomial_zsmul_add
- Nyll.AlgebraicCurves.Foundations.Polynomial.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
- Nyll.AlgebraicCurves.Foundations.Polynomial.Algebra_levelSet_finite_free_finrank_of_flat_polynomial
- Nyll.AlgebraicCurves.Foundations.Polynomial.LaurentPolynomial_isUnit_iff_exists_C_mul_T
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_exists_forall_eval_ne_zero_macaulayPow_finrank_piece_sup_add_le
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_exists_forall_eval_ne_zero_mem_of_mul_mem_and_finrank_piece_sup_eq_macaulayPow
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_exists_forall_eval_ne_zero_mem_of_mul_mem_of_finrank_piece_succ_eq_macaulayPow
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_exists_forall_sum_C_mul_X_mul_mem_imp_of_forall_exists_X_pow_mul_mem
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_exists_ne_zero_and_forall_irreducible_map_of_irreducible_map_algebraicClosure
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_exists_skew_eq_sum_mul_X_of_sum_mul_X_eq_zero
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_exists_span_monomial_finrank_piece_eq_and_finrank_piece_succ_eq_macaulayPow
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_finrank_piece_add_two_eq_macaulayPow_of_finrank_piece_succ_eq_macaulayPow
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_finrank_piece_eq_of_maximal_growth
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_finrank_piece_succ_le_macaulayPow
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_finrank_piece_sup_span_singleton_succ_add_finrank_piece_eq_of_forall_mul_mem_imp
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_forall_finrank_piece_succ_eq_macaulayPow_of_finrank_piece_succ_eq_macaulayPow
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_isHomogeneous_of_forall_eval_intCast_mul_eq_pow_mul
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_le_finrank_piece_of_forall_succ_eq_macaulayPow_of_eventually_eq
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_mem_span_of_linear_mul_mem_of_forall_relation_modulo_mem_span
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_relation_mem_span_of_forall_isHomogeneous_mem_span
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_relation_mem_span_of_linear_of_forall_relation_modulo_mem_span
- Nyll.AlgebraicCurves.Foundations.Polynomial.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
- Nyll.AlgebraicCurves.Foundations.Polynomial.Polynomial_irreducible_map_map_algebraicClosure_of_separable_of_forall_isSeparable_mem_range
- Nyll.AlgebraicCurves.Foundations.Polynomial.RingHom_laurentSeries_derivative_eq_of_kaehlerDifferential_D_eq_smul
- Nyll.AlgebraicCurves.Foundations.Polynomial.fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_exists_ne_zero_common_zero_of_card_lt
- Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_exists_ne_zero_eval_eq_zero_of_finrank_lt
Imported by1
This module has no indexed declarations. Its imports and full source are available here.