Commit 2021-01-27 21:59 3e599600

View on Github →

feat(ring_theory/nullstellensatz): Classical Nullstellensatz (#5760) This file states and proves Hilbert's classical nullstellensatz for multi-variate polynomials over an algebraically closed field.

Estimated changes

Modified docs/overview.yaml

Modified src/field_theory/algebraic_closure.lean

added theorem is_alg_closed.algebra_map_surjective_of_is_integral'

Modified src/ring_theory/jacobson.lean

Created src/ring_theory/nullstellensatz.lean

added theorem mv_polynomial.is_maximal_iff_eq_vanishing_ideal_singleton

added theorem mv_polynomial.is_prime.vanishing_ideal_zero_locus

added theorem mv_polynomial.le_vanishing_ideal_zero_locus

added theorem mv_polynomial.mem_vanishing_ideal_iff

added theorem mv_polynomial.mem_vanishing_ideal_singleton_iff

added theorem mv_polynomial.mem_zero_locus_iff

added def mv_polynomial.point_to_point

added theorem mv_polynomial.point_to_point_zero_locus_le

added theorem mv_polynomial.radical_le_vanishing_ideal_zero_locus

added def mv_polynomial.vanishing_ideal

added theorem mv_polynomial.vanishing_ideal_anti_mono

added theorem mv_polynomial.vanishing_ideal_empty

added theorem mv_polynomial.vanishing_ideal_point_to_point

added theorem mv_polynomial.vanishing_ideal_zero_locus_eq_radical

added def mv_polynomial.zero_locus

added theorem mv_polynomial.zero_locus_anti_mono

added theorem mv_polynomial.zero_locus_bot

added theorem mv_polynomial.zero_locus_top

added theorem mv_polynomial.zero_locus_vanishing_ideal_galois_connection

added theorem mv_polynomial.zero_locus_vanishing_ideal_le