Module

AddCommGroup_apply_zsmul_add_eq_of_forall_cube.lean

Nyll.AlgebraicCurves.Foundations.Algebra.AddCommGroup_apply_zsmul_add_eq_of_forall_cube

5 declarations indexed from sourceView source ↗

Module documentation

Add Comm Group apply zsmul add eq of forall cube

Imports5

Mathlib.Algebra.Module.NatInt
Mathlib.Tactic.Abel
Mathlib.Tactic.Module
Mathlib.Tactic.NormNum
Mathlib.Tactic.Ring.RingNF

Imported by2

theorem

tri_succ

L31 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_apply_zsmul_add_eq_of_forall_cube.P2mQuad.tri_succ

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_apply_zsmul_add_eq_of_forall_cube
namespace P2mQuad
variable {M N : Type*} [AddCommGroup M] [AddCommGroup N]

Lean source · statement

theorem tri_succ (n : ℤ) : (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n

theorem

tri_zero

L35 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_apply_zsmul_add_eq_of_forall_cube.P2mQuad.tri_zero

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_apply_zsmul_add_eq_of_forall_cube
namespace P2mQuad
variable {M N : Type*} [AddCommGroup M] [AddCommGroup N]

Lean source · statement

theorem tri_zero : (0 : ℤ) * (0 - 1) / 2 = 0

theorem

eq_of_second_difference

L37 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_apply_zsmul_add_eq_of_forall_cube.P2mQuad.eq_of_second_difference

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_apply_zsmul_add_eq_of_forall_cube
namespace P2mQuad
variable {M N : Type*} [AddCommGroup M] [AddCommGroup N]

Lean source · statement

theorem eq_of_second_difference (g : ℤ → N) (D : N)
    (h : ∀ n : ℤ, g (n + 2) - 2 • g (n + 1) + g n = D) (n : ℤ) :
    g n = g 0 + n • (g 1 - g 0) + (n * (n - 1) / 2) • D

theorem

main

L83 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_apply_zsmul_add_eq_of_forall_cube.P2mQuad.main

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_apply_zsmul_add_eq_of_forall_cube
namespace P2mQuad
variable {M N : Type*} [AddCommGroup M] [AddCommGroup N]

Lean source · statement

theorem main (Λ : M → N)
    (hΛ : ∀ x y z : M, Λ (x + y + z) - Λ (x + y) - Λ (x + z) - Λ (y + z) + Λ x + Λ y + Λ z = Λ 0)
    (x y : M) (n : ℤ) :
    Λ (n • x + y) = Λ y + n • (Λ (x + y) - Λ y) + (n * (n - 1) / 2) • (Λ (2 • x) - 2 • Λ x + Λ 0)

theorem

apply_zsmul_add_eq_of_forall_cube

L112 ↗

AddCommGroup.apply_zsmul_add_eq_of_forall_cube

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.AddCommGroup_apply_zsmul_add_eq_of_forall_cube

Lean source · statement

theorem _root_.AddCommGroup.apply_zsmul_add_eq_of_forall_cube
    {M N : Type*} [AddCommGroup M] [AddCommGroup N] (Λ : M → N)
    (hΛ : ∀ x y z : M,
      Λ (x + y + z) - Λ (x + y) - Λ (x + z) - Λ (y + z) + Λ x + Λ y + Λ z = Λ 0)
    (x y : M) (n : ℤ) :
    Λ (n • x + y) =
      Λ y + n • (Λ (x + y) - Λ y) + (n * (n - 1) / 2) • (Λ (2 • x) - 2 • Λ x + Λ 0)

Module documentation

Add Comm Group apply zsmul add eq of forall cube

Declarations

tri_succ

tri_zero

eq_of_second_difference

main

apply_zsmul_add_eq_of_forall_cube