Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-29 00:28 bab38133

View on Github →

feat(ring_theory/PID): PIDs and xgcd for ED (#298)

Estimated changes

Modified algebra/euclidean_domain.lean

added def euclidean_domain.gcd_a

added def euclidean_domain.gcd_b

added theorem euclidean_domain.gcd_eq_gcd_ab

added theorem euclidean_domain.mod_eq_sub_mul_div

added def euclidean_domain.xgcd

added def euclidean_domain.xgcd_aux

added theorem euclidean_domain.xgcd_aux_P

added theorem euclidean_domain.xgcd_aux_fst

added theorem euclidean_domain.xgcd_aux_rec

added theorem euclidean_domain.xgcd_aux_val

added theorem euclidean_domain.xgcd_val

added theorem euclidean_domain.xgcd_zero_left

Modified algebra/ring.lean

added theorem zero_dvd_iff

Created ring_theory/PID.lean

added theorem is_prime_ideal.to_maximal_ideal

added theorem is_principal_ideal.eq_trivial_iff_generator_eq_zero

added theorem is_principal_ideal.generator_generates

added theorem is_principal_ideal.generator_mem

added theorem is_principal_ideal.mem_iff_generator_dvd

added theorem mod_mem_iff

Modified ring_theory/ideals.lean

added theorem is_ideal.mem_trivial

modified theorem is_maximal_ideal.mk

modified theorem is_proper_ideal_iff_one_not_mem

modified theorem quotient_ring.eq_zero_iff_mem