Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-25 15:09 81207e09

View on Github →

feat(algebra/triv_sq_zero_ext): trivial square-zero extension (#5109)

Estimated changes

Created src/algebra/triv_sq_zero_ext.lean

added theorem triv_sq_zero_ext.ext

added def triv_sq_zero_ext.fst

added theorem triv_sq_zero_ext.fst_add

added def triv_sq_zero_ext.fst_hom

added theorem triv_sq_zero_ext.fst_inl

added theorem triv_sq_zero_ext.fst_inr

added theorem triv_sq_zero_ext.fst_mul

added theorem triv_sq_zero_ext.fst_neg

added theorem triv_sq_zero_ext.fst_one

added theorem triv_sq_zero_ext.fst_smul

added theorem triv_sq_zero_ext.fst_zero

added def triv_sq_zero_ext.inl

added theorem triv_sq_zero_ext.inl_add

added theorem triv_sq_zero_ext.inl_fst_add_inr_snd_eq

added def triv_sq_zero_ext.inl_hom

added theorem triv_sq_zero_ext.inl_injective

added theorem triv_sq_zero_ext.inl_mul

added theorem triv_sq_zero_ext.inl_mul_inl

added theorem triv_sq_zero_ext.inl_mul_inr

added theorem triv_sq_zero_ext.inl_neg

added theorem triv_sq_zero_ext.inl_one

added theorem triv_sq_zero_ext.inl_zero

added def triv_sq_zero_ext.inr

added theorem triv_sq_zero_ext.inr_add

added def triv_sq_zero_ext.inr_hom

added theorem triv_sq_zero_ext.inr_injective

added theorem triv_sq_zero_ext.inr_mul_inl

added theorem triv_sq_zero_ext.inr_mul_inr

added theorem triv_sq_zero_ext.inr_neg

added theorem triv_sq_zero_ext.inr_smul

added theorem triv_sq_zero_ext.inr_zero

added def triv_sq_zero_ext.snd

added theorem triv_sq_zero_ext.snd_add

added theorem triv_sq_zero_ext.snd_inl

added theorem triv_sq_zero_ext.snd_inr

added theorem triv_sq_zero_ext.snd_mul

added theorem triv_sq_zero_ext.snd_neg

added theorem triv_sq_zero_ext.snd_one

added theorem triv_sq_zero_ext.snd_smul

added theorem triv_sq_zero_ext.snd_zero

added def triv_sq_zero_ext