Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-14 00:37 77e52484

View on Github →

feat(algebra/triv_sq_zero_ext): universal property (#10754)

Estimated changes

Modified src/algebra/triv_sq_zero_ext.lean

added theorem triv_sq_zero_ext.alg_hom_ext'

added theorem triv_sq_zero_ext.alg_hom_ext

added theorem triv_sq_zero_ext.ind

added def triv_sq_zero_ext.lift

added def triv_sq_zero_ext.lift_aux

added theorem triv_sq_zero_ext.lift_aux_apply_inr

added theorem triv_sq_zero_ext.lift_aux_comp_inr_hom

added theorem triv_sq_zero_ext.lift_aux_inr_hom

added theorem triv_sq_zero_ext.linear_map_ext