Commit 2023-03-15 10:21 8b2910f3

View on Github →

feat: port Algebra.Algebra.Unitization (#2892)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Algebra/Unitization.lean

added def NonUnitalAlgHom.toAlgHom

added theorem Unitization.algHom_ext'

added theorem Unitization.algHom_ext

added theorem Unitization.algebraMap_eq_inl

added theorem Unitization.algebraMap_eq_inlRingHom_comp

added theorem Unitization.algebraMap_eq_inl_comp

added theorem Unitization.algebraMap_eq_inl_hom

added theorem Unitization.ext

added def Unitization.fst

added def Unitization.fstHom

added theorem Unitization.fst_add

added theorem Unitization.fst_inl

added theorem Unitization.fst_inr

added theorem Unitization.fst_mul

added theorem Unitization.fst_neg

added theorem Unitization.fst_one

added theorem Unitization.fst_smul

added theorem Unitization.fst_star

added theorem Unitization.fst_zero

added theorem Unitization.ind

added def Unitization.inl

added def Unitization.inlRingHom

added theorem Unitization.inl_add

added theorem Unitization.inl_fst_add_inr_snd_eq

added theorem Unitization.inl_injective

added theorem Unitization.inl_mul

added theorem Unitization.inl_mul_inl

added theorem Unitization.inl_mul_inr

added theorem Unitization.inl_neg

added theorem Unitization.inl_one

added theorem Unitization.inl_smul

added theorem Unitization.inl_star

added theorem Unitization.inl_zero

added def Unitization.inr

added def Unitization.inrHom

added def Unitization.inrNonUnitalAlgHom

added theorem Unitization.inr_add

added theorem Unitization.inr_injective

added theorem Unitization.inr_mul

added theorem Unitization.inr_mul_inl

added theorem Unitization.inr_neg

added theorem Unitization.inr_smul

added theorem Unitization.inr_star

added theorem Unitization.inr_zero

added def Unitization.lift

added theorem Unitization.lift_symm_apply_apply

added theorem Unitization.linearMap_ext

added def Unitization.snd

added def Unitization.sndHom

added theorem Unitization.snd_add

added theorem Unitization.snd_inl

added theorem Unitization.snd_inr

added theorem Unitization.snd_mul

added theorem Unitization.snd_neg

added theorem Unitization.snd_one

added theorem Unitization.snd_smul

added theorem Unitization.snd_star

added theorem Unitization.snd_zero

added def Unitization