Commit 2023-07-03 00:43 4ebd604d

View on Github →

feat: define NonUnitalSubalgebra and develop basic API (#5512) This continues the non-unital-ization of mathlib.

depends on: #5151

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

added def NonUnitalAlgHom.codRestrict

added theorem NonUnitalAlgHom.coe_codRestrict

added theorem NonUnitalAlgHom.coe_range

added def NonUnitalAlgHom.equalizer

added theorem NonUnitalAlgHom.injective_codRestrict

added theorem NonUnitalAlgHom.mem_equalizer

added theorem NonUnitalAlgHom.mem_range

added theorem NonUnitalAlgHom.mem_range_self

added def NonUnitalAlgHom.rangeRestrict

added theorem NonUnitalAlgHom.range_comp

added theorem NonUnitalAlgHom.range_comp_le_range

added theorem NonUnitalAlgHom.subtype_comp_codRestrict

added def NonUnitalAlgebra.adjoin

added theorem NonUnitalAlgebra.adjoin_empty

added theorem NonUnitalAlgebra.adjoin_induction'

added theorem NonUnitalAlgebra.adjoin_induction

added theorem NonUnitalAlgebra.adjoin_induction₂

added theorem NonUnitalAlgebra.adjoin_le

added theorem NonUnitalAlgebra.adjoin_le_iff

added theorem NonUnitalAlgebra.adjoin_toSubmodule

added theorem NonUnitalAlgebra.adjoin_union

added theorem NonUnitalAlgebra.adjoin_univ

added theorem NonUnitalAlgebra.coe_bot

added theorem NonUnitalAlgebra.coe_iInf

added theorem NonUnitalAlgebra.coe_inf

added theorem NonUnitalAlgebra.coe_sInf

added theorem NonUnitalAlgebra.coe_top

added theorem NonUnitalAlgebra.comap_top

added theorem NonUnitalAlgebra.eq_top_iff

added theorem NonUnitalAlgebra.iInf_toSubmodule

added theorem NonUnitalAlgebra.inf_toNonUnitalSubsemiring

added theorem NonUnitalAlgebra.inf_toSubmodule

added theorem NonUnitalAlgebra.map_bot

added theorem NonUnitalAlgebra.map_sup

added theorem NonUnitalAlgebra.map_top

added theorem NonUnitalAlgebra.mem_bot

added theorem NonUnitalAlgebra.mem_iInf

added theorem NonUnitalAlgebra.mem_inf

added theorem NonUnitalAlgebra.mem_sInf

added theorem NonUnitalAlgebra.mem_sup_left

added theorem NonUnitalAlgebra.mem_sup_right

added theorem NonUnitalAlgebra.mem_top

added theorem NonUnitalAlgebra.mul_mem_sup

added theorem NonUnitalAlgebra.range_id

added theorem NonUnitalAlgebra.range_top_iff_surjective

added theorem NonUnitalAlgebra.sInf_toNonUnitalSubsemiring

added theorem NonUnitalAlgebra.sInf_toSubmodule

added theorem NonUnitalAlgebra.self_mem_adjoin_singleton

added theorem NonUnitalAlgebra.subset_adjoin

added theorem NonUnitalAlgebra.toNonUnitalSubsemiring_eq_top

added theorem NonUnitalAlgebra.toSubmodule_bot

added theorem NonUnitalAlgebra.toSubmodule_eq_top

added def NonUnitalAlgebra.toTop

added theorem NonUnitalAlgebra.to_subring_eq_top

added theorem NonUnitalAlgebra.top_toNonUnitalSubsemiring

added theorem NonUnitalAlgebra.top_toSubmodule

added theorem NonUnitalAlgebra.top_toSubring

added def NonUnitalSubalgebra.center

added theorem NonUnitalSubalgebra.center_eq_top

added theorem NonUnitalSubalgebra.center_toNonUnitalSubring

added theorem NonUnitalSubalgebra.center_toNonUnitalSubsemiring

added def NonUnitalSubalgebra.centralizer

added theorem NonUnitalSubalgebra.centralizer_le

added theorem NonUnitalSubalgebra.centralizer_univ

added theorem NonUnitalSubalgebra.coe_center

added theorem NonUnitalSubalgebra.coe_centralizer

added theorem NonUnitalSubalgebra.coe_comap

added theorem NonUnitalSubalgebra.coe_copy

added theorem NonUnitalSubalgebra.coe_iSup_of_directed

added theorem NonUnitalSubalgebra.coe_inclusion

added theorem NonUnitalSubalgebra.coe_map

added theorem NonUnitalSubalgebra.coe_prod

added theorem NonUnitalSubalgebra.coe_smul

added theorem NonUnitalSubalgebra.coe_toNonUnitalSubring

added theorem NonUnitalSubalgebra.coe_toNonUnitalSubsemiring

added theorem NonUnitalSubalgebra.coe_toSubmodule

added def NonUnitalSubalgebra.comap

added theorem NonUnitalSubalgebra.copy_eq

added theorem NonUnitalSubalgebra.ext

added theorem NonUnitalSubalgebra.gc_map_comap

added theorem NonUnitalSubalgebra.iSupLift_comp_inclusion

added theorem NonUnitalSubalgebra.iSupLift_inclusion

added theorem NonUnitalSubalgebra.iSupLift_mk

added theorem NonUnitalSubalgebra.iSupLift_of_mem

added def NonUnitalSubalgebra.inclusion

added theorem NonUnitalSubalgebra.inclusion_inclusion

added theorem NonUnitalSubalgebra.inclusion_injective

added theorem NonUnitalSubalgebra.inclusion_mk

added theorem NonUnitalSubalgebra.inclusion_right

added theorem NonUnitalSubalgebra.inclusion_self

added def NonUnitalSubalgebra.map

added theorem NonUnitalSubalgebra.map_id

added theorem NonUnitalSubalgebra.map_injective

added theorem NonUnitalSubalgebra.map_le

added theorem NonUnitalSubalgebra.map_map

added theorem NonUnitalSubalgebra.map_mono

added theorem NonUnitalSubalgebra.map_toNonUnitalSubsemiring

added theorem NonUnitalSubalgebra.map_toSubmodule

added theorem NonUnitalSubalgebra.mem_carrier

added theorem NonUnitalSubalgebra.mem_center_iff

added theorem NonUnitalSubalgebra.mem_centralizer_iff

added theorem NonUnitalSubalgebra.mem_comap

added theorem NonUnitalSubalgebra.mem_map

added theorem NonUnitalSubalgebra.mem_prod

added theorem NonUnitalSubalgebra.mem_toNonUnitalSubring

added theorem NonUnitalSubalgebra.mem_toNonUnitalSubsemiring

added theorem NonUnitalSubalgebra.mem_toSubmodule

added def NonUnitalSubalgebra.prod

added theorem NonUnitalSubalgebra.prod_inf_prod

added theorem NonUnitalSubalgebra.prod_mono

added theorem NonUnitalSubalgebra.prod_toSubmodule

added theorem NonUnitalSubalgebra.prod_top

added theorem NonUnitalSubalgebra.range_val

added def NonUnitalSubalgebra.toNonUnitalSubring'

added def NonUnitalSubalgebra.toNonUnitalSubring

added theorem NonUnitalSubalgebra.toNonUnitalSubring_inj

added theorem NonUnitalSubalgebra.toNonUnitalSubring_injective

added def NonUnitalSubalgebra.toNonUnitalSubsemiring'

added theorem NonUnitalSubalgebra.toNonUnitalSubsemiring_inj

added theorem NonUnitalSubalgebra.toNonUnitalSubsemiring_injective

added theorem NonUnitalSubalgebra.toNonUnitalSubsemiring_subtype

added def NonUnitalSubalgebra.toSubmodule'

added def NonUnitalSubalgebra.toSubmoduleEquiv

added theorem NonUnitalSubalgebra.toSubmodule_inj

added theorem NonUnitalSubalgebra.toSubmodule_injective

added theorem NonUnitalSubalgebra.toSubmodule_toNonUnitalSubalgebra

added theorem NonUnitalSubalgebra.toSubring_subtype

added structure NonUnitalSubalgebra

added theorem NonUnitalSubalgebraClass.coeSubtype

added def NonUnitalSubalgebraClass.subtype

added theorem Set.smul_mem_center

added theorem Set.smul_mem_centralizer

added theorem Submodule.coe_toNonUnitalSubalgebra

added theorem Submodule.mem_toNonUnitalSubalgebra

added def Submodule.toNonUnitalSubalgebra

added theorem Submodule.toNonUnitalSubalgebra_mk

added theorem Submodule.toNonUnitalSubalgebra_toSubmodule

added theorem mem_nonUnitalSubalgebraOfNonUnitalSubring

added theorem mem_nonUnitalSubalgebraOfNonUnitalSubsemiring

added def nonUnitalSubalgebraOfNonUnitalSubring

added def nonUnitalSubalgebraOfNonUnitalSubsemiring

Modified Mathlib/Algebra/Hom/NonUnitalAlg.lean

added theorem NonUnitalAlgHom.coe_id

Modified Mathlib/Algebra/Module/Submodule/Basic.lean

added def SMulMemClass.toModule'

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

added def SMulMemClass.ofIsScalarTower

Modified Mathlib/LinearAlgebra/Span.lean

added theorem Submodule.span_induction₂