`BookProof.TensorPerm.purePow_ne_zero` {n : ℕ} {f : Fin n → E.carrier} (hf : ∀ i, f i ≠ 0) : purePow E n f ≠ 0

Initializing...

`BookProof.TensorPerm.purePow_ne_zero` {n : ℕ} {f : Fin n → E.carrier} (hf : ∀ i, f i ≠ 0) : purePow E n f ≠ 0 · Prove2Me