Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-22 10:12 f3a4c480

View on Github →

feat(algebra/subalgebra): missing norm_cast lemmas about operations (#6790)

Estimated changes

added theorem subalgebra.coe_add
added theorem subalgebra.coe_eq_one
added theorem subalgebra.coe_eq_zero
added theorem subalgebra.coe_mul
added theorem subalgebra.coe_neg
added theorem subalgebra.coe_one
added theorem subalgebra.coe_pow
added theorem subalgebra.coe_smul
added theorem subalgebra.coe_sub
added theorem subalgebra.coe_zero
added theorem subsemiring.coe_add
modified theorem subsemiring.coe_mul
modified theorem subsemiring.coe_one
added theorem subsemiring.coe_pow
added theorem subsemiring.coe_zero