Commit 2023-02-21 09:05 3ce8f3f7

View on Github →

feat: port RingTheory.Ideal.Basic (#2283) This only needs the dependency below in one place (otherwise LinearAlgebra.Span suffices as a replacement import). This file is done otherwise. porting notes:

to appease the simpNF linter, I increased the priority of a few simp lemmas
The lean 4 issue 2074 appeared in (only one!) place in this file. I worked around it for now and left a note.

depends on: #2277

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Ideal/Basic.lean

added theorem Ideal.IsMaximal.coprime_of_ne

added theorem Ideal.IsMaximal.eq_of_le

added theorem Ideal.IsMaximal.exists_inv

added theorem Ideal.IsMaximal.isPrime

added theorem Ideal.IsMaximal.ne_top

added theorem Ideal.IsPrime.mem_of_pow_mem

added theorem Ideal.IsPrime.mem_or_mem

added theorem Ideal.IsPrime.mem_or_mem_of_mul_eq_zero

added theorem Ideal.IsPrime.mul_mem_iff_mem_or_mem

added theorem Ideal.IsPrime.ne_top

added theorem Ideal.IsPrime.pow_mem_iff_mem

added theorem Ideal.bot_isMaximal

added theorem Ideal.bot_lt_of_maximal

added theorem Ideal.bot_prime

added theorem Ideal.eq_bot_of_prime

added theorem Ideal.eq_bot_or_top

added theorem Ideal.eq_top_iff_one

added theorem Ideal.eq_top_of_isUnit_mem

added theorem Ideal.eq_top_of_unit_mem

added theorem Ideal.exists_le_maximal

added theorem Ideal.exists_maximal

added theorem Ideal.ext

added theorem Ideal.factors_decreasing

added theorem Ideal.infₛ_isPrime_of_isChain

added theorem Ideal.isMaximal_def

added theorem Ideal.isMaximal_iff

added theorem Ideal.isPrime_iff

added theorem Ideal.maximal_of_no_maximal

added theorem Ideal.mem_bot

added theorem Ideal.mem_inf

added theorem Ideal.mem_infᵢ

added theorem Ideal.mem_infₛ

added theorem Ideal.mem_pi

added theorem Ideal.mem_span

added theorem Ideal.mem_span_insert'

added theorem Ideal.mem_span_insert

added theorem Ideal.mem_span_pair

added theorem Ideal.mem_span_singleton'

added theorem Ideal.mem_span_singleton

added theorem Ideal.mem_span_singleton_self

added theorem Ideal.mem_span_singleton_sup

added theorem Ideal.mem_sup_left

added theorem Ideal.mem_sup_right

added theorem Ideal.mem_supᵢ_of_mem

added theorem Ideal.mem_supₛ_of_mem

added theorem Ideal.mul_mem_left

added theorem Ideal.mul_mem_right

added theorem Ideal.mul_sub_mul_mem

added theorem Ideal.mul_unit_mem_iff_mem

added theorem Ideal.ne_top_iff_one

added theorem Ideal.not_isPrime_iff

added def Ideal.ofRel

added def Ideal.pi

added theorem Ideal.pow_mem_of_mem

added theorem Ideal.pow_multiset_sum_mem_span_pow

added def Ideal.span

added theorem Ideal.span_empty

added theorem Ideal.span_eq

added theorem Ideal.span_eq_bot

added theorem Ideal.span_eq_top_iff_finite

added theorem Ideal.span_insert

added theorem Ideal.span_le

added theorem Ideal.span_mono

added theorem Ideal.span_one

added theorem Ideal.span_pair_add_mul_left

added theorem Ideal.span_pair_add_mul_right

added theorem Ideal.span_pair_comm

added theorem Ideal.span_pow_eq_top

added theorem Ideal.span_singleton_eq_bot

added theorem Ideal.span_singleton_eq_span_singleton

added theorem Ideal.span_singleton_eq_top

added theorem Ideal.span_singleton_le_iff_mem

added theorem Ideal.span_singleton_le_span_singleton

added theorem Ideal.span_singleton_lt_span_singleton

added theorem Ideal.span_singleton_mul_left_unit

added theorem Ideal.span_singleton_mul_right_unit

added theorem Ideal.span_singleton_ne_top

added theorem Ideal.span_singleton_neg

added theorem Ideal.span_singleton_one

added theorem Ideal.span_singleton_prime

added theorem Ideal.span_union

added theorem Ideal.span_unionᵢ

added theorem Ideal.span_univ

added theorem Ideal.span_zero

added theorem Ideal.submodule_span_eq

added theorem Ideal.subset_span

added theorem Ideal.sum_mem

added theorem Ideal.sum_pow_mem_span_pow

added theorem Ideal.unit_mul_mem_iff_mem

added theorem Ideal.zero_ne_one_of_proper

added def Ideal

added theorem Ring.exists_not_isUnit_of_not_isField

added theorem Ring.isField_iff_isSimpleOrder_ideal

added theorem Ring.ne_bot_of_isMaximal_of_not_isField

added theorem Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top

added theorem Ring.not_isField_iff_exists_prime

added theorem coe_subset_nonunits

added theorem exists_max_ideal_of_mem_nonunits

added theorem mem_nonunits_iff

added theorem mul_mem_nonunits_left

added theorem mul_mem_nonunits_right

added def nonunits

added theorem one_not_mem_nonunits

added theorem zero_mem_nonunits