Theorem Fin.removeNth_fun_const

Modification history

2025-11-26 01:45
Mathlib/Data/Fin/Tuple/Basic.lean
feat(DifferentialForm): pullback commutes with exterior derivative (#30871)
Added Fin.removeNth_fun_constView on Github →