Commit 2021-06-09 10:12 86766851

View on Github →

feat(ring_theory): every left-noetherian ring satisfies the strong rank condition (#7711) This PR also discards the proof that every left-noetherian ring satisfies the rank condition, because we already have in #7683 that this implies that.

Estimated changes

Modified src/algebra/lie/abelian.lean

Modified src/algebra/module/submodule_lattice.lean

added def submodule.bot_equiv_punit

added def submodule.top_equiv_self

Modified src/analysis/normed_space/inner_product.lean

Modified src/data/equiv/basic.lean

added theorem equiv.sum_arrow_equiv_prod_arrow_apply_fst

added theorem equiv.sum_arrow_equiv_prod_arrow_apply_snd

added theorem equiv.sum_arrow_equiv_prod_arrow_symm_apply_inl

added theorem equiv.sum_arrow_equiv_prod_arrow_symm_apply_inr

Modified src/data/set/disjointed.lean

added theorem pairwise_disjoint_on_nat

added theorem pairwise_on_nat

Modified src/linear_algebra/basic.lean

added theorem submodule.comap_inf_map_of_injective

added theorem submodule.comap_infi_map_of_injective

added theorem submodule.comap_map_eq_of_injective

added theorem submodule.comap_sup_map_of_injective

added theorem submodule.comap_supr_map_of_injective

added theorem submodule.comap_surjective_of_injective

added def submodule.gci_map_comap

added theorem submodule.map_injective_of_injective

added theorem submodule.map_le_map_iff_of_injective

added theorem submodule.map_strict_mono_of_injective

Modified src/linear_algebra/invariant_basis_number.lean

Modified src/linear_algebra/pi.lean

added def linear_equiv.sum_arrow_lequiv_prod_arrow

added theorem linear_equiv.sum_arrow_lequiv_prod_arrow_apply_fst

added theorem linear_equiv.sum_arrow_lequiv_prod_arrow_apply_snd

added theorem linear_equiv.sum_arrow_lequiv_prod_arrow_symm_apply_inl

added theorem linear_equiv.sum_arrow_lequiv_prod_arrow_symm_apply_inr

Modified src/linear_algebra/prod.lean

added def linear_map.tailing

added theorem linear_map.tailing_disjoint_tunnel_succ

added theorem linear_map.tailing_le_tunnel

added def linear_map.tailing_linear_equiv

added theorem linear_map.tailing_sup_tunnel_succ_le_tunnel

added def linear_map.tailings

added theorem linear_map.tailings_disjoint_tailing

added theorem linear_map.tailings_disjoint_tunnel

added theorem linear_map.tailings_succ

added theorem linear_map.tailings_zero

added def linear_map.tunnel

added def linear_map.tunnel_aux

added theorem linear_map.tunnel_aux_injective

added def submodule.fst

added def submodule.fst_equiv

added theorem submodule.fst_inf_snd

added theorem submodule.fst_map_fst

added theorem submodule.fst_map_snd

added theorem submodule.fst_sup_snd

added def submodule.snd

added def submodule.snd_equiv

added theorem submodule.snd_map_fst

added theorem submodule.snd_map_snd

Modified src/logic/unique.lean

Modified src/order/bounded_lattice.lean

added theorem eq_bot_of_disjoint_absorbs

Modified src/order/modular_lattice.lean

added theorem disjoint.disjoint_sup_left_of_disjoint_sup_right

Created src/order/partial_sups.lean

added theorem le_partial_sups

added def partial_sups

added theorem partial_sups_disjoint_of_disjoint

added theorem partial_sups_eq

added theorem partial_sups_le

added theorem partial_sups_succ

added theorem partial_sups_zero

Modified src/ring_theory/noetherian.lean

modified theorem finite_of_linear_independent

modified theorem is_noetherian.bijective_of_surjective_endomorphism

added theorem is_noetherian.disjoint_partial_sups_eventually_bot

modified theorem is_noetherian.induction

modified theorem is_noetherian.injective_of_surjective_endomorphism

modified theorem is_noetherian_iff_well_founded

modified theorem monotone_stabilizes_iff_noetherian

modified theorem set_has_maximal_iff_noetherian