Commit 2023-03-10 13:47 da1f9e08

View on Github →

feat: port Algebra.Algebra.Subalgebra.Basic (#2743)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

added theorem AlgEquiv.ofInjective_apply

added def AlgEquiv.ofLeftInverse

added theorem AlgEquiv.ofLeftInverse_apply

added theorem AlgEquiv.ofLeftInverse_symm_apply

added def AlgEquiv.subalgebraMap

added def AlgHom.codRestrict

added theorem AlgHom.coe_codRestrict

added theorem AlgHom.coe_range

added def AlgHom.equalizer

added theorem AlgHom.injective_codRestrict

added theorem AlgHom.mem_equalizer

added theorem AlgHom.mem_range

added theorem AlgHom.mem_range_self

added def AlgHom.rangeRestrict

added theorem AlgHom.range_comp

added theorem AlgHom.range_comp_le_range

added theorem AlgHom.val_comp_codRestrict

added def Algebra.adjoin

added theorem Algebra.bijective_algebraMap_iff

added theorem Algebra.coe_bot

added theorem Algebra.coe_inf

added theorem Algebra.coe_infᵢ

added theorem Algebra.coe_infₛ

added theorem Algebra.coe_top

added theorem Algebra.comap_top

added theorem Algebra.eq_top_iff

added theorem Algebra.inf_toSubmodule

added theorem Algebra.inf_toSubsemiring

added theorem Algebra.infᵢ_toSubmodule

added theorem Algebra.infₛ_toSubmodule

added theorem Algebra.infₛ_toSubsemiring

added theorem Algebra.map_bot

added theorem Algebra.map_sup

added theorem Algebra.map_top

added theorem Algebra.mem_bot

added theorem Algebra.mem_inf

added theorem Algebra.mem_infᵢ

added theorem Algebra.mem_infₛ

added theorem Algebra.mem_sup_left

added theorem Algebra.mem_sup_right

added theorem Algebra.mem_top

added theorem Algebra.mul_mem_sup

added theorem Algebra.range_id

added theorem Algebra.range_top_iff_surjective

added theorem Algebra.surjective_algebraMap_iff

added theorem Algebra.toSubmodule_bot

added theorem Algebra.toSubmodule_eq_top

added theorem Algebra.toSubring_eq_top

added theorem Algebra.toSubsemiring_eq_top

added def Algebra.toTop

added theorem Algebra.top_toSubmodule

added theorem Algebra.top_toSubring

added theorem Algebra.top_toSubsemiring

added theorem Set.algebraMap_mem_center

added theorem Set.algebraMap_mem_centralizer

added theorem Subalgebra.algebraMap_eq

added theorem Subalgebra.algebraMap_mem

added def Subalgebra.center

added theorem Subalgebra.center_eq_top

added theorem Subalgebra.center_toSubring

added theorem Subalgebra.center_toSubsemiring

added def Subalgebra.centralizer

added theorem Subalgebra.centralizer_le

added theorem Subalgebra.centralizer_univ

added theorem Subalgebra.coe_algebraMap

added theorem Subalgebra.coe_center

added theorem Subalgebra.coe_centralizer

added theorem Subalgebra.coe_comap

added theorem Subalgebra.coe_copy

added theorem Subalgebra.coe_inclusion

added theorem Subalgebra.coe_map

added theorem Subalgebra.coe_prod

added theorem Subalgebra.coe_smul

added theorem Subalgebra.coe_supᵢ_of_directed

added theorem Subalgebra.coe_toSubmodule

added theorem Subalgebra.coe_toSubring

added theorem Subalgebra.coe_toSubsemiring

added theorem Subalgebra.coe_val

added def Subalgebra.comap

added theorem Subalgebra.copy_eq

added def Subalgebra.equivOfEq

added theorem Subalgebra.equivOfEq_rfl

added theorem Subalgebra.equivOfEq_symm

added theorem Subalgebra.equivOfEq_trans

added theorem Subalgebra.ext

added theorem Subalgebra.gc_map_comap

added def Subalgebra.inclusion

added theorem Subalgebra.inclusion_inclusion

added theorem Subalgebra.inclusion_injective

added theorem Subalgebra.inclusion_mk

added theorem Subalgebra.inclusion_right

added theorem Subalgebra.inclusion_self

added def Subalgebra.map

added theorem Subalgebra.map_id

added theorem Subalgebra.map_injective

added theorem Subalgebra.map_le

added theorem Subalgebra.map_map

added theorem Subalgebra.map_mono

added theorem Subalgebra.map_toSubmodule

added theorem Subalgebra.map_toSubsemiring

added theorem Subalgebra.mem_carrier

added theorem Subalgebra.mem_center_iff

added theorem Subalgebra.mem_centralizer_iff

added theorem Subalgebra.mem_comap

added theorem Subalgebra.mem_map

added theorem Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem

added theorem Subalgebra.mem_of_span_eq_top_of_smul_pow_mem

added theorem Subalgebra.mem_prod

added theorem Subalgebra.mem_toSubmodule

added theorem Subalgebra.mem_toSubring

added theorem Subalgebra.mem_toSubsemiring

added def Subalgebra.prod

added theorem Subalgebra.prod_inf_prod

added theorem Subalgebra.prod_mono

added theorem Subalgebra.prod_toSubmodule

added theorem Subalgebra.prod_top

added theorem Subalgebra.rangeS_algebraMap

added theorem Subalgebra.rangeS_le

added theorem Subalgebra.range_algebraMap

added theorem Subalgebra.range_le

added theorem Subalgebra.range_subset

added theorem Subalgebra.range_val

added theorem Subalgebra.smul_def

added theorem Subalgebra.smul_mem

added theorem Subalgebra.supᵢLift_comp_inclusion

added theorem Subalgebra.supᵢLift_inclusion

added theorem Subalgebra.supᵢLift_mk

added theorem Subalgebra.supᵢLift_of_mem

added def Subalgebra.toAddSubmonoid

added def Subalgebra.toSubmodule

added def Subalgebra.toSubmoduleEquiv

added theorem Subalgebra.toSubmodule_toSubalgebra

added def Subalgebra.toSubring

added theorem Subalgebra.toSubring_inj

added theorem Subalgebra.toSubring_injective

added theorem Subalgebra.toSubring_subtype

added theorem Subalgebra.toSubsemiring_inj

added theorem Subalgebra.toSubsemiring_injective

added theorem Subalgebra.toSubsemiring_subtype

added def Subalgebra.topEquiv

added def Subalgebra.val

added theorem Subalgebra.val_apply

added structure Subalgebra

added theorem Submodule.coe_toSubalgebra

added theorem Submodule.mem_toSubalgebra

added def Submodule.toSubalgebra

added theorem Submodule.toSubalgebra_mk

added theorem Submodule.toSubalgebra_toSubmodule

added theorem mem_subalgebraOfSubring

added theorem mem_subalgebraOfSubsemiring

added def subalgebraOfSubring

added def subalgebraOfSubsemiring

Modified Mathlib/RingTheory/Subsemiring/Basic.lean