EuclideanSpace.single 2 1 ≠ 0

Stream: new members

[ZhiKai Pong]

import Mathlib

example : EuclideanSpace.single (2 : Fin 3) (1 : ℝ) ≠ 0 := by
  intro h
  have := congr_fun h 2
  simp at this

this is the shortest proof I can come up, I was expecting this to be solved by a simple simp but apparently not, should I be surprised? otherwise, is there a more elegant way?

[Eric Wieser]

There are a few trivial missing lemmas here, will paste in a second

[Eric Wieser]

import Mathlib

@[simp]
theorem WithLp.equiv_symm_eq_zero_iff {p V} [AddCommGroup V] {v : V} :
    (WithLp.equiv p V).symm v = 0 ↔ v = 0 := Iff.rfl

@[simp]
theorem WithLp.equiv_eq_zero_iff {p V} [AddCommGroup V] {v : WithLp p V} :
    WithLp.equiv p V v = 0 ↔ v = 0 := Iff.rfl

@[simp]
theorem EuclideanSpace.single_eq_zero_iff {ι 𝕜} [RCLike 𝕜] [DecidableEq ι] {i : ι} {x : 𝕜} :
    EuclideanSpace.single i x = 0 ↔ x = 0 := Pi.single_eq_zero_iff

example : EuclideanSpace.single (2 : Fin 3) (1 : ℝ) ≠ 0 := by
  simp

[ZhiKai Pong]

@Eric Wieser should I make a PR? it's your code so I'm not sure whether I should do it on your behalf

[Eric Wieser]

Please do!

[ZhiKai Pong]

#25552