k : Type u_1
inst✝⁹ : Ring k
V : Type u_2
P : Type u_3
V₁ : Type ?u.23420
P₁ : Type ?u.23423
V₂ : Type ?u.23426
P₂ : Type ?u.23429
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
v : V
s : AffineSubspace k P
⊢ Submodule.map (↑(AffineEquiv.constVAdd k P v)).linear (direction s) = direction s
k : Type u_1
inst✝⁹ : Ring k
V : Type u_2
P : Type u_3
V₁ : Type ?u.23420
P₁ : Type ?u.23423
V₂ : Type ?u.23426
P₂ : Type ?u.23429
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
v : V
s : AffineSubspace k P
⊢ direction (v +ᵥ s) = direction s
rw [pointwise_vadd_eq_map, map_direction]
no goals
k : Type u_1
inst✝⁹ : Ring k
V : Type u_2
P : Type u_3
V₁ : Type ?u.23420
P₁ : Type ?u.23423
V₂ : Type ?u.23426
P₂ : Type ?u.23429
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AffineSpace V P
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
v : V
s : AffineSubspace k P
⊢ Submodule.map (↑(AffineEquiv.constVAdd k P v)).linear (direction s) = direction s
exact Submodule.map_id _