Theorem: AffineEquiv.coe_VSubconst (src/Pre.lean)

State before:
𝕜 E P : Type
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : AddTorsor E P
x : P
⊢ ⇑(VSubconst 𝕜 x) = fun x_1 => x_1 -ᵥ x
Tactic:
rfl
State after:
no goals