case h.mk
K : Type u_2
V : Type u_1
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type ?u.156698
W : Type ?u.156701
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
x✝ : ℙ K V
v : { v // v ≠ 0 }
⊢ map LinearMap.id (_ : Function.Injective ↑(LinearEquiv.refl K V)) (Quot.mk Setoid.r v) = id (Quot.mk Setoid.r v)
K : Type u_2
V : Type u_1
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type ?u.156698
W : Type ?u.156701
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
⊢ map LinearMap.id (_ : Function.Injective ↑(LinearEquiv.refl K V)) = id
ext ⟨v⟩
no goals
case h.mk
K : Type u_2
V : Type u_1
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type ?u.156698
W : Type ?u.156701
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
x✝ : ℙ K V
v : { v // v ≠ 0 }
⊢ map LinearMap.id (_ : Function.Injective ↑(LinearEquiv.refl K V)) (Quot.mk Setoid.r v) = id (Quot.mk Setoid.r v)
rfl