Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-13 10:49 a945b376

View on Github →

feat(data/sym/basic): add fill filter_ne and sigma_ext (#16316) Add definitions and lemmas to support a proof for the multinomial theorem.

Estimated changes

added def sym.append
added theorem sym.append_comm
added theorem sym.append_inj_left
added theorem sym.append_inj_right
added theorem sym.cast_cast
added theorem sym.cast_rfl
added theorem sym.coe_cast
added def sym.fill
added def sym.filter_ne
added theorem sym.sigma_sub_ext