mathlib3 documentation

linear_algebra.affine_space.pointwise

Pointwise instances on affine_subspaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides the additive action affine_subspace.pointwise_add_action in the pointwise locale.

@[protected]
def affine_subspace.pointwise_add_action {k : Type u_1} [ring k] {V : Type u_2} {P : Type u_3} [add_comm_group V] [module k V] [add_torsor V P] :

The additive action on an affine subspace corresponding to applying the action to every element.

This is available as an instance in the pointwise locale.

Equations
@[simp]
theorem affine_subspace.coe_pointwise_vadd {k : Type u_1} [ring k] {V : Type u_2} {P : Type u_3} [add_comm_group V] [module k V] [add_torsor V P] (v : V) (s : affine_subspace k P) :
(v +ᵥ s) = v +ᵥ s
theorem affine_subspace.vadd_mem_pointwise_vadd_iff {k : Type u_1} [ring k] {V : Type u_2} {P : Type u_3} [add_comm_group V] [module k V] [add_torsor V P] {v : V} {s : affine_subspace k P} {p : P} :
v +ᵥ p v +ᵥ s p s
theorem affine_subspace.pointwise_vadd_bot {k : Type u_1} [ring k] {V : Type u_2} {P : Type u_3} [add_comm_group V] [module k V] [add_torsor V P] (v : V) :
theorem affine_subspace.pointwise_vadd_direction {k : Type u_1} [ring k] {V : Type u_2} {P : Type u_3} [add_comm_group V] [module k V] [add_torsor V P] (v : V) (s : affine_subspace k P) :
theorem affine_subspace.pointwise_vadd_span {k : Type u_1} [ring k] {V : Type u_2} {P : Type u_3} [add_comm_group V] [module k V] [add_torsor V P] (v : V) (s : set P) :
theorem affine_subspace.map_pointwise_vadd {k : Type u_1} [ring k] {V₁ : Type u_4} {P₁ : Type u_5} {V₂ : Type u_6} {P₂ : Type u_7} [add_comm_group V₁] [module k V₁] [add_torsor V₁ P₁] [add_comm_group V₂] [module k V₂] [add_torsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (v : V₁) (s : affine_subspace k P₁) :