Mathlib v3 is deprecated. Go to Mathlib v4

Theorem fin.append_right_eq_snoc

Modification history

2023-03-30 12:15
src/data/fin/tuple/basic.lean
feat(linear_algebra/tensor_power): the tensor powers form a graded algebra (#10255)
Added fin.append_right_eq_snocView on Github →