AffineMap.ext
theorem AffineMap.ext :
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
[inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
[inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] {f g : P1 →ᵃ[k] P2}, (∀ (p : P1), f p = g p) → f = g
This theorem states that two affine maps are equal if they map every point in their domain to the same point in their codomain. More formally, for any type `k` forming a ring, types `V1` and `V2` forming additive commutative groups and being modules over `k`, types `P1` and `P2` being affine spaces over `V1` and `V2` respectively, and any two affine maps `f` and `g` from `P1` to `P2`, if for every point `p` in `P1`, `f` of `p` equals `g` of `p`, then `f` and `g` are equal.
More concisely: If two affine maps between modules over a commutative ring and their corresponding affine spaces map every point to the same image, then they are equal.
|
AffineMap.linearMap_vsub
theorem AffineMap.linearMap_vsub :
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
[inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
[inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p1 p2 : P1),
f.linear (p1 -ᵥ p2) = f p1 -ᵥ f p2
This theorem states that for any affine map `f`, which maps points in an affine space `P1` over a ring `k` to another affine space `P2`, and any two points `p1` and `p2` in `P1`, applying the linear map associated with `f` to the vector obtained by subtracting `p2` from `p1` is the same as subtracting the image of `p2` (under `f`) from the image of `p1` (under `f`). In other words, the action of the linear map on the difference of two points in the original space corresponds to the difference of their images in the target space.
More concisely: For any affine map f from an affine space P1 over a ring k to an affine space P2, the linear map associated with f maps the difference of any two points in P1 to the difference of their images in P2.
|
AffineMap.apply_lineMap
theorem AffineMap.apply_lineMap :
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
[inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
[inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) (c : k),
f ((AffineMap.lineMap p₀ p₁) c) = (AffineMap.lineMap (f p₀) (f p₁)) c
The theorem `AffineMap.apply_lineMap` states that for any ring `k`, any additive commutative groups `V1` and `V2`, any `k`-modules `V1` and `V2`, and any affine spaces `P1` and `P2` over `V1` and `V2` respectively, and for any affine map `f` from `P1` to `P2`, any points `p₀` and `p₁` in `P1`, and any scalar `c` in `k`, applying `f` to the result of the affine line map from `k` to `P1` at `c`, which sends `0` to `p₀` and `1` to `p₁`, is equal to the result of the affine line map from `k` to `P2` at `c`, which sends `0` to `f p₀` and `1` to `f p₁`. In other words, the diagram commutes, meaning that the order in which we apply the affine map and the line map does not matter.
More concisely: For any affine maps `f` and affine line maps `λ_p0` and `λ_p1` with base points `p0` and `p1` respectively, the diagram commutes, that is, `λ_p1(c) ∘ f = f ∘ λ_p0(c)` for all scalars `c`.
|
AffineMap.lineMap_apply_zero
theorem AffineMap.lineMap_apply_zero :
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
[inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1), (AffineMap.lineMap p₀ p₁) 0 = p₀
This theorem states that for any type `k` forming a ring, type `V1` forming an additive commutative group, and an affine space `P1` formed over the vector space `V1` and the field `k`, the affine map `lineMap`, which maps `0` to a point `p₀` and `1` to a point `p₁`, when applied to `0`, always yields `p₀`. In other words, the `lineMap` function associates the scalar `0` with the initial point of the line segment in the affine space.
More concisely: For any ring `k`, additive commutative group `V1`, and affine space `P1` over `V1` and `k`, the affine map `lineMap` from `k` to `P1` satisfies `lineMap 0 = p₀`.
|
AffineMap.lineMap_apply_one
theorem AffineMap.lineMap_apply_one :
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
[inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1), (AffineMap.lineMap p₀ p₁) 1 = p₁
The theorem `AffineMap.lineMap_apply_one` states that for any two points `p₀` and `p₁` in an affine space `P1`, the affine map defined by `lineMap p₀ p₁` sends the scalar `1` to the point `p₁`. Here, `P1` is a type representing an affine space, `V1` is a type representing the associated vector space, and `k` is the type representing the underlying field of scalars. The space `P1` is assumed to be a torsor over the vector space `V1` (given by `inst_3 : AddTorsor V1 P1`). The operation of the affine map on `1` directly gives the end point `p₁` of the line segment defined by `p₀` and `p₁`.
More concisely: For any affine space P1 over a field k with associated vector space V1 and given points p0 and p1, the affine map lineMap p0 p1 sends the scalar 1 to point p1.
|
Convex.combo_affine_apply
theorem Convex.combo_affine_apply :
∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Ring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
[inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] {x y : E} {a b : 𝕜} {f : E →ᵃ[𝕜] F},
a + b = 1 → f (a • x + b • y) = a • f x + b • f y
This theorem states that if you have an affine map 'f' from a scalar field '𝕜' to two different types 'E' and 'F' (which are additive commutative groups and also 𝕜-modules), two points 'x' and 'y' in 'E', and two scalars 'a' and 'b' in '𝕜' that add up to 1, then applying the affine map 'f' to the affine combination a*x + b*y equals the affine combination of the images a*f(x) + b*f(y). Thus, the effect of the affine map 'f' is distributive over the affine combination of the points.
More concisely: Given an affine map f from a commutative ring R to additive groups and R-modules E and F, and points x, y in E and scalars a, b in R with a + b = 1, then af(x) + bf(y) = f(ax + by).
|
AffineMap.lineMap_apply_one_sub
theorem AffineMap.lineMap_apply_one_sub :
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
[inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1) (c : k),
(AffineMap.lineMap p₀ p₁) (1 - c) = (AffineMap.lineMap p₁ p₀) c
This theorem states that for any ring `k`, additive commutative group `V1`, and affine torsor `P1`, given any two points `p₀` and `p₁` in `P1` and any scalar `c` in `k`, the result of applying the affine map `lineMap` that maps `0` to `p₀` and `1` to `p₁`, to the scalar `(1 - c)` is the same as the result of applying the affine map `lineMap` that maps `0` to `p₁` and `1` to `p₀`, to the scalar `c`. In other words, it illustrates a kind of symmetry in how the `lineMap` function operates on points and scalars in an affine space.
More concisely: For any ring `k`, additive commutative group `V1`, affine torsor `P1`, points `p₀, p₁ ∈ P1`, and scalar `c ∈ k`, `lineMap(0, p₀, p₁)(1 - c) = lineMap(0, p₁, p₀)(c)`.
|
AffineMap.comp_apply
theorem AffineMap.comp_apply :
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7}
[inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1]
[inst_4 : AddCommGroup V2] [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] [inst_7 : AddCommGroup V3]
[inst_8 : Module k V3] [inst_9 : AddTorsor V3 P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) (p : P1),
(f.comp g) p = f (g p)
This theorem states that for any ring `k`, affine spaces `P1`, `P2`, and `P3` over the vector spaces `V1`, `V2`, and `V3` respectively, and affine maps `f : P2 →ᵃ[k] P3` and `g : P1 →ᵃ[k] P2`, the composition of `f` and `g` applied to a point `p` in `P1` equals the application of `f` to the result of applying `g` to `p`. In other words, `(f.comp g) p = f (g p)`, which is the standard rule for function composition in mathematics.
More concisely: For any rings `k`, affine spaces `P1`, `P2`, `P3` over vector spaces `V1`, `V2`, `V3`, and affine maps `f : P2 →ᵃ[k] P3` and `g : P1 →ᵃ[k] P2`, the map composition `f ∘ g` equals the function application `f ∘ (g(•))`, i.e., `(f ∘ g) (p) = f (g(p))` for any point `p` in `P1`.
|
AffineMap.lineMap_apply
theorem AffineMap.lineMap_apply :
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
[inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1) (c : k), (AffineMap.lineMap p₀ p₁) c = c • (p₁ -ᵥ p₀) +ᵥ p₀
The theorem `AffineMap.lineMap_apply` states that for any type `k` endowed with a ring structure, any type `V1` endowed with an additive commutative group structure, any `k`-module `V1`, any type `P1` that forms an affine space with `V1`, and any two points `p₀` and `p₁` in `P1`, applying the affine map `AffineMap.lineMap p₀ p₁` to a scalar `c` in `k` results in the point obtained by adding `p₀` to the vector obtained by scaling the difference vector `p₁ -ᵥ p₀` by `c`. In mathematical notation, this is `(AffineMap.lineMap p₀ p₁) c = c • (p₁ -ᵥ p₀) +ᵥ p₀`.
More concisely: Given an affine space `P1` over a ring `k` with base vector space `V1`, and points `p₀` and `p₁` in `P1`, the affine map `AffineMap.lineMap p₀ p₁` satisfies `(AffineMap.lineMap p₀ p₁) c = c * (p₁ - p₀) + p₀`, where `c` is a scalar in `k`.
|
AffineMap.lineMap_apply_module
theorem AffineMap.lineMap_apply_module :
∀ {k : Type u_1} {V1 : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] (p₀ p₁ : V1)
(c : k), (AffineMap.lineMap p₀ p₁) c = (1 - c) • p₀ + c • p₁
The theorem `AffineMap.lineMap_apply_module` states that for any ring `k`, an additive commutative group `V1`, a module `k V1`, two points `p₀` and `p₁` in `V1`, and any scalar `c` in `k`, applying the affine map `lineMap` defined from `k` to `P1` with `p₀` and `p₁` to `c` gives the result `(1 - c) • p₀ + c • p₁`. In other words, the output of `lineMap` for a scalar input interpolates linearly between `p₀` and `p₁` according to the scalar.
More concisely: For any ring `k`, additive commutative group `V1`, module `k V1`, points `p₀, p₁ ∈ V1`, and scalar `c ∈ k`, the application of the affine map `lineMap` on `k V1` defined by `p₀` and `p₁` to the scalar `c` equals `(1 - c) • p₀ + c • p₁`.
|
AffineMap.decomp
theorem AffineMap.decomp :
∀ {k : Type u_1} {V1 : Type u_2} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
[inst_3 : AddCommGroup V2] [inst_4 : Module k V2] (f : V1 →ᵃ[k] V2), ⇑f = ⇑f.linear + fun x => f 0
This theorem, named `AffineMap.decomp`, states that for any affine map `f` from one vector space `V1` to another vector space `V2` over a ring `k`, the application of `f` can be decomposed into the sum of the application of the linear part of `f` and the application of `f` to zero. Here, both vector spaces `V1` and `V2` are also assumed to be additively commutative groups.
More concisely: For any affine map f from vector space V1 to vector space V2 over ring k, f(x) = L(x) + f(0), where L is the linear part of f.
|
AffineMap.decomp'
theorem AffineMap.decomp' :
∀ {k : Type u_1} {V1 : Type u_2} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
[inst_3 : AddCommGroup V2] [inst_4 : Module k V2] (f : V1 →ᵃ[k] V2), ⇑f.linear = ⇑f - fun x => f 0
This theorem is about the decomposition of an affine map in a specific case where the point space and vector space are identical. It states that for any affine map `f` from vector space `V1` to `V2` over a ring `k`, the linear part of `f` is equal to the function obtained by subtracting `f 0` from `f`. In other words, it shows that any affine map can be decomposed into a linear map and a translation.
More concisely: For an affine map `f` from vector space `V` to `V` over a ring `k`, the linear part of `f` equals `f` minus the constant map `f 0`.
|
AffineMap.lineMap_same_apply
theorem AffineMap.lineMap_same_apply :
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
[inst_3 : AddTorsor V1 P1] (p : P1) (c : k), (AffineMap.lineMap p p) c = p
This theorem states that for any point `p` in an affine space `P1` over a ring `k` with an associated vector space `V1`, when the affine map `lineMap` is constructed from `p` to `p` (i.e., both the start and end points are the same), the image of any element `c` from the ring `k` under this map is `p` itself. Essentially, this means that a line map from a point to the same point maps all scalars to that point.
More concisely: For any point `p` in an affine space `P1` over a ring `k` with associated vector space `V1`, the affine map `lineMap` constructed from `p` to `p` maps any scalar `c` from `k` to point `p` itself.
|
AffineMap.coe_id
theorem AffineMap.coe_id :
∀ (k : Type u_1) {V1 : Type u_2} (P1 : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
[inst_3 : AddTorsor V1 P1], ⇑(AffineMap.id k P1) = id
The theorem `AffineMap.coe_id` asserts that for any ring `k`, any additive commutative group `V1`, any `k`-module `V1`, and any affine space `P1` over `V1`, the identity affine map, denoted by `AffineMap.id k P1`, behaves exactly as the identity function. In other words, if you apply this identity affine map to any point in the affine space `P1`, it returns the same point.
More concisely: The identity affine map on an affine space over a ring and its associated vector space is the identity function.
|
AffineMap.coe_comp
theorem AffineMap.coe_comp :
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7}
[inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1]
[inst_4 : AddCommGroup V2] [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] [inst_7 : AddCommGroup V3]
[inst_8 : Module k V3] [inst_9 : AddTorsor V3 P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2), ⇑(f.comp g) = ⇑f ∘ ⇑g
This theorem, `AffineMap.coe_comp`, states that for any ring `k` and affine spaces `P1`, `P2`, and `P3` over vector spaces `V1`, `V2`, and `V3` respectively, the composition of two affine maps (from `P2` to `P3` and from `P1` to `P2`) is the same as applying the two functions in sequence. This is analogous to function composition in the context of affine maps.
More concisely: Given rings `k`, affine spaces `P1` over `V1`, `P2` over `V2`, and `P3` over `V3`, and affine maps `f : P2 -> P3` and `g : P1 -> P2`, the composition of `f` and `g` equals the function `h : P1 -> P3` defined by `h := f ∘ g`.
|
AffineMap.toFun_eq_coe
theorem AffineMap.toFun_eq_coe :
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
[inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
[inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] P2), f.toFun = ⇑f
This theorem states that for any affine map `f` mapping points from type `P1` to `P2` in a given ring `k`, the function `toFun` applied to `f` is exactly the same as coercing `f` to a function. This applies in the context where `V1` and `V2` are additive commutative groups, `P1` and `P2` are affine spaces (or torsors) over `V1` and `V2` respectively, and `V1` and `V2` are modules over the ring `k`.
More concisely: For any affine maps between affine spaces over a commutative ring, the function obtained by applying `toFun` is equivalent to the coercion of the map to a function between the spaces.
|
AffineMap.lineMap_eq_lineMap_iff
theorem AffineMap.lineMap_eq_lineMap_iff :
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
[inst_3 : AddTorsor V1 P1] [inst_4 : NoZeroSMulDivisors k V1] {p₀ p₁ : P1} {c₁ c₂ : k},
(AffineMap.lineMap p₀ p₁) c₁ = (AffineMap.lineMap p₀ p₁) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
The theorem `AffineMap.lineMap_eq_lineMap_iff` states that for any ring `k`, any additive commutative group `V1`, any module of `k` over `V1`, any additive torsor `V1` over `P1`, and any non-zero scalar multiplication divisor of `k` over `V1`, if `p₀` and `p₁` are two points in `P1` and `c₁` and `c₂` are two scalars in `k`, then the affine map from `k` to `P1` that sends `0` to `p₀` and `1` to `p₁`, evaluated at `c₁`, equals the same affine map evaluated at `c₂` if and only if either `p₀` equals `p₁` or `c₁` equals `c₂`.
More concisely: For any ring `k`, additive commutative group `V1`, module `M` over `k` as an `AddMonoidWithCarrier` over `V1`, additive torsor `V1` over a group `P1`, and non-zero scalar multiplication divisor `r` over `V1`, the affine maps from `k` to `P1` that send `0` to `p0` and `1` to `p1`, are equal if and only if `p0 = p1` or `c1 = c2`, where `c1` and `c2` are scalars in `k`.
|
AffineMap.id_apply
theorem AffineMap.id_apply :
∀ (k : Type u_1) {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
[inst_3 : AddTorsor V1 P1] (p : P1), (AffineMap.id k P1) p = p
The theorem `AffineMap.id_apply` states that for any type `k` equipped with a ring structure, any type `V1` with an additive commutative group structure, any module `V1` over `k`, any type `P1` which is an affine space over `V1`, and any point `p` in `P1`, applying the identity affine map (as defined by `AffineMap.id`) to the point `p` results in the point `p` itself. In other words, the identity affine map truly acts as the identity, leaving every point unchanged.
More concisely: The identity affine map of an affine space over a ring-equipped type leaves every point unchanged.
|
AffineMap.lineMap_vsub_left
theorem AffineMap.lineMap_vsub_left :
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
[inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1) (c : k), (AffineMap.lineMap p₀ p₁) c -ᵥ p₀ = c • (p₁ -ᵥ p₀)
This theorem states that for any three points `p₀`, `p₁`, and `c` in an affine space `P1` over a ring `k`, with `P1` being a module over `k` and an additive torsor for an additive commutative group `V1`, the difference vector from `p₀` to the point on the line from `p₀` to `p₁` determined by `c` (`(AffineMap.lineMap p₀ p₁) c -ᵥ p₀`) is equal to the scalar multiple `c` times the difference vector from `p₀` to `p₁` (`c • (p₁ -ᵥ p₀)`). In other words, it describes the property of affine maps that linearly interpolate between points in an affine space.
More concisely: For any points `p₀`, `p₁` in an affine space `P1` over a ring `k`, and any scalar `c`, the vector `(AffineMap.lineMap p₀ p₁) c -ᵥ p₀` equals `c • (p₁ -ᵥ p₀)`.
|
AffineMap.map_vadd
theorem AffineMap.map_vadd :
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
[inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
[inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p : P1) (v : V1),
f (v +ᵥ p) = f.linear v +ᵥ f p
This theorem states that for any ring `k`, additively commutative groups `V1` and `V2`, modules `V1` and `V2` over `k`, additively commutative torsor `P1` over `V1` and `P2` over `V2`, and an affine map `f` from `P1` to `P2`, the result of applying the affine map `f` to the sum of a vector `v` from `V1` and a point `p` from `P1` is equivalent to the sum of the result of applying the linear part of `f` to `v` and the result of applying `f` to `p`.
More concisely: For any ring `k`, additively commutative groups `V1` and `V2`, modules `V1` and `V2` over `k`, additively commutative torsors `P1` over `V1` and `P2` over `V2`, and an affine map `f` from `P1` to `P2`, we have `f(p + v) = f(p) + fⁱ(v)`, where `fⁱ` denotes the linear part of `f`.
|
AffineMap.coe_mk
theorem AffineMap.coe_mk :
∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
[inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
[inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 → P2) (linear : V1 →ₗ[k] V2)
(add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = linear v +ᵥ f p),
⇑{ toFun := f, linear := linear, map_vadd' := add } = f
This theorem states that for any set of parameters -- including two types `P1` and `P2` representing points, two types `V1` and `V2` representing vectors, a type `k` forming a ring, two functions `f` and `linear`, and an addition operation `add` -- constructing an affine map and then coercing it back into a function yields the original function `f`. In mathematical terms, if we view an affine map as a matrix operator with `f` as the translation vector and `linear` as the linear part, the theorem states that applying the affine map to a vector plus a point is the same as first applying the linear part to the vector, then adding the resulting vector to the point transformed by `f`.
More concisely: Given an affine map defined by a linear transformation and a translation vector, applying the map to a point-vector pair is equivalent to first performing the linear transformation on the vector and then translating the resulting vector using the translation vector.
|