Normalizing a tuple at a nonzero entry

Over a semifield, dividing the other entries of a tuple b : Fin (n + 1) → k by a nonzero entry b i and reinserting 1 in position i gives (b i)⁻¹ • b. This is the normalization used by the standard affine charts of projective space and by dehomogenization of polynomials.

Main results

• Fin.insertNth_one_div_eq_inv_smul: reinserting 1 at a nonzero coordinate into the coordinate ratios recovers the tuple scaled by the inverse of that coordinate.

theorem Fin.insertNth_one_div_eq_inv_smul {k : Type u_1} [Semifield k] {n : ℕ} (i : Fin (n + 1)) (b : Fin (n + 1) → k) (hi : b i ≠ 0) : (i.insertNth 1 fun (j : Fin n) => b (i.succAbove j) / b i) = (b i)⁻¹ • b

Reinserting one at a nonzero coordinate into the coordinate ratios recovers the homogeneous coordinates scaled by the inverse of that coordinate.