Commit 2023-03-12 08:31 48c5b56d

View on Github →

feat: port RingTheory.Adjoin.Basic (#2817)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Adjoin/Basic.lean

added theorem AlgHom.adjoin_le_equalizer

added theorem AlgHom.ext_of_adjoin_eq_top

added theorem AlgHom.map_adjoin

added def Algebra.adjoinCommRingOfComm

added def Algebra.adjoinCommSemiringOfComm

added theorem Algebra.adjoin_adjoin_coe_preimage

added theorem Algebra.adjoin_adjoin_of_tower

added theorem Algebra.adjoin_attach_bunionᵢ

added theorem Algebra.adjoin_empty

added theorem Algebra.adjoin_eq

added theorem Algebra.adjoin_eq_infₛ

added theorem Algebra.adjoin_eq_of_le

added theorem Algebra.adjoin_eq_ring_closure

added theorem Algebra.adjoin_eq_span

added theorem Algebra.adjoin_eq_span_of_subset

added theorem Algebra.adjoin_image

added theorem Algebra.adjoin_induction'

added theorem Algebra.adjoin_induction

added theorem Algebra.adjoin_induction₂

added theorem Algebra.adjoin_inl_union_inr_eq_prod

added theorem Algebra.adjoin_insert_adjoin

added theorem Algebra.adjoin_int

added theorem Algebra.adjoin_le

added theorem Algebra.adjoin_le_iff

added theorem Algebra.adjoin_mono

added theorem Algebra.adjoin_prod_le

added theorem Algebra.adjoin_singleton_one

added theorem Algebra.adjoin_span

added theorem Algebra.adjoin_toSubmodule_le

added theorem Algebra.adjoin_union

added theorem Algebra.adjoin_union_coe_submodule

added theorem Algebra.adjoin_union_eq_adjoin_adjoin

added theorem Algebra.adjoin_unionᵢ

added theorem Algebra.adjoin_univ

added theorem Algebra.mem_adjoin_iff

added theorem Algebra.mem_adjoin_of_map_mul

added theorem Algebra.pow_smul_mem_adjoin_smul

added theorem Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin

added theorem Algebra.self_mem_adjoin_singleton

added theorem Algebra.span_le_adjoin

added theorem Algebra.subset_adjoin