Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-01 15:31 6010cf52

View on Github →

feat(ring_theory/dedekind_domain): lemmas for showing Dedekind domains are PIDs (#18301) This PR includes a few lemmas that prove certain Dedekind domains are PIDs. These will be useful for showing the ideal norm map is multiplicative. Co-Authored-By: Riccardo Brasca riccardo.brasca@gmail.com

Estimated changes

Modified src/algebra/algebra/operations.lean

added theorem submodule.mem_mul_span_singleton

added theorem submodule.mem_span_singleton_mul

Modified src/algebra/module/submodule/bilinear.lean

added theorem submodule.map₂_flip

added theorem submodule.map₂_span_singleton_eq_map

added theorem submodule.map₂_span_singleton_eq_map_flip

Modified src/ring_theory/dedekind_domain/ideal.lean

added theorem is_dedekind_domain.exists_forall_sub_mem_ideal

added theorem is_dedekind_domain.exists_representative_mod_finset

Created src/ring_theory/dedekind_domain/pid.lean

added theorem fractional_ideal.is_principal.of_finite_maximals_of_inv

added theorem fractional_ideal.is_principal_of_unit_of_comap_mul_span_singleton_eq_top

added theorem ideal.eq_span_singleton_of_mem_of_not_mem_sq_of_not_mem_prime_ne

added theorem ideal.is_principal.of_finite_maximals_of_is_unit

added theorem is_dedekind_domain.is_principal_ideal_ring_localization_over_prime

added theorem is_localization.over_prime.mem_normalized_factors_of_is_prime

added theorem is_principal_ideal_ring.of_finite_primes

Modified src/ring_theory/fractional_ideal.lean

added theorem fractional_ideal.one_le

added theorem fractional_ideal.span_singleton_le_iff_mem

Modified src/ring_theory/ideal/basic.lean

added theorem ideal.is_maximal.coprime_of_ne

Modified src/ring_theory/ideal/operations.lean

added theorem ideal.multiset_prod_span_singleton

Modified src/ring_theory/principal_ideal_domain.lean

added theorem is_principal_ideal_ring.of_prime

added def non_principals

added theorem non_principals_def

added theorem non_principals_eq_empty_iff

added theorem non_principals_zorn