Schule

This file defines torsors of additive group actions.

Notation

The group elements are referred to as acting on points. This file defines the notation +ᵥ for adding a group element to a point and -ᵥ for subtracting two points to produce a group element.

Implementation notes

Affine spaces are the motivating example of torsors of additive group actions. It may be appropriate to refactor in terms of the general definition of group actions, via to_additive, when there is a use for multiplicative torsors (currently mathlib only develops the theory of group actions for multiplicative group actions).

Notation

• v +ᵥ p is a notation for VAdd.vadd, the left action of an additive monoid;

• p₁ -ᵥ p₂ is a notation for VSub.vsub, difference between two points in an additive torsor as an element of the corresponding additive group;

References

• https://en.wikipedia.org/wiki/Principal_homogeneous_space
• https://en.wikipedia.org/wiki/Affine_space

theorem Schule.zweite_lemma (x : ℝ) : x + 100 * x ^ 2 + 120 * x ^ 2 + 1 = 220 * x ^ 2 + 1 + x

Beispiel 2

theorem Schule.dritte_lemma (a b : ℝ) : (2 * a + b) ^ 2 = 4 * a ^ 2 + 4 * a * b + b ^ 2

Beispiel 3

theorem Schule.frac_mul {R : Type u_1} [Field R] (a b c d : R) (hb : b ≠ 0) (hd : d ≠ 0) : a / b * (c / d) = a * c / (b * d)

das soll da erscheinen3!! $$ \frac{a}{b} \cdot \frac{c}{d} = \frac{a \cdot c}{b \cdot d} $$

theorem Schule.axiom_mul_inv_cancel {R : Type u_1} [g : Field R] (a : R) (h : a ≠ 0) : a * a⁻¹ = 1

theorem Schule.ff {R : Type u_1} [Field R] (a b : R) (ha : a ≠ 0) (hb : b ≠ 0) : (a * b)⁻¹ = a⁻¹ * b⁻¹

theorem Schule.lemma6 : 1 / 321 * (1 / (3 * 1)) = 1 * 1 / (321 * (3 * 1))

@[irreducible]

def Schule.gcd (m n : ℕ) : ℕ

Equations

• Schule.gcd m n = if m = 0 then n else Schule.gcd (n % m) m

theorem Schule.my_zpow_add11 {G : Type u_1} [GroupWithZero G] (a : G) (m n : ℤ) (h1 : m ≥ 0) (h2 : n ≥ 0) : a ^ (m + n) = a ^ m * a ^ n

theorem Schule.my_pow_add {M : Type u_1} [Monoid M] (x : M) (a b : ℕ) : x ^ (a + b) = x ^ a * x ^ b

theorem Schule.my_zpow_add1 {G : Type u_1} [GroupWithZero G] {x : G} {a b : ℤ} (h1 : a ≥ 0) (h2 : b ≥ 0) : x ^ (a + b) = x ^ a * x ^ b

theorem Schule.my_zpow_add2 {G : Type u_1} [GroupWithZero G] (x : G) (a b : ℤ) (h : x ≠ 0) : x ^ (a + b) = x ^ a * x ^ b

theorem Schule.my_rpow_add {x : ℝ} (hx : x > 0) (a b : ℝ) : x ^ (a + b) = x ^ a * x ^ b

theorem Schule.my_add_left_neg {G : Type} [g : AddGroup G] (a : G) : -a + a = 0

theorem Schule.my_mul_left_neg {G : Type} [g : Group G] (a : G) : a⁻¹ * a = 1

theorem Schule.tt {G : Type} [g : DivInvMonoid G] (a : G) : a⁻¹ = 1 / a