Mul

Theorems about multiplication in ring-like structures.

Some of them require one or several properties:

rngl_mul_is_comm T = true : that the multiplication is commutative,
rngl_has_opp T = true : that there is an opposite
rngl_has_psub T = true : that there is a partial subtraction,
rngl_has_opp_or_psub T = true : that there is an opposite or a partial subtraction,

See the module RingLike.Core for the general description of the ring-like library.

In general, it is not necessary to import this module. The normal usage is to do:

    Require Import RingLike.Core.

which imports the present module and some other ones.

From Stdlib Require Import Utf8 Arith.
Require Import Structures.
Require Import Add.

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.

Theorem rngl_mul_comm :
  rngl_mul_is_comm T = true →
  ∀ a b, (a × b = b × a)%L.

Theorem rngl_mul_add_distr_r : ∀ x y z,
  ((x + y ) × z = x × z + y × z)%L.
Theorem rngl_mul_0_r :
  rngl_has_opp_or_psub T = true →
  ∀ a, (a × 0 = 0)%L.

Theorem rngl_mul_0_r' :
  rngl_has_psub T = true →
  (∀ a b c, a × (b - c ) = a × b - a × c)%L
  → ∀ a, (a × 0 = 0)%L.

Theorem rngl_mul_0_r'' :
  rngl_has_psub T = true →
  ∀ a, (a × 0 = 0)%L.

Theorem rngl_mul_0_l :
  rngl_has_opp_or_psub T = true →
  ∀ a, (0 × a = 0)%L.

Theorem rngl_mul_1_r : ∀ a, (a × 1 = a)%L.

Theorem rngl_mul_2_l : ∀ a, (2 × a = a + a)%L.

Theorem rngl_mul_2_r : ∀ a, (a × 2 = a + a)%L.

Theorem rngl_mul_mul_swap :
  rngl_mul_is_comm T = true →
  ∀ a b c, (a × b × c = a × c × b)%L.

Theorem rngl_mul_opp_r :
  rngl_has_opp T = true →
  ∀ a b, (a × - b = - (a × b ))%L.

Theorem rngl_mul_sub_distr_l :
  rngl_has_opp T = true →
  ∀ a b c, (a × (b - c ) = a × b - a × c)%L.

Theorem rngl_add_mul_r_diag_l : ∀ a b, (a + a × b = a × (1 + b ))%L.

Theorem rngl_add_mul_r_diag_r : ∀ a b, (a + b × a = (1 + b ) × a)%L.

Theorem rngl_add_mul_l_diag_l : ∀ a b, (a × b + a = a × (b + 1))%L.

Theorem rngl_add_mul_l_diag_r : ∀ a b, (a × b + b = (a + 1) × b)%L.

Theorem rngl_sub_mul_r_diag_l :
  rngl_has_opp T = true →
  ∀ a b, (a - a × b = a × (1 - b ))%L.

Theorem rngl_sub_mul_l_diag_l :
  rngl_has_opp T = true →
  ∀ a b : T, (a × b - a)%L = (a × (b - 1))%L.

Theorem rngl_mul_opp_l :
  rngl_has_opp T = true →
  ∀ a b, (- a × b = - (a × b ))%L.

Theorem rngl_mul_sub_distr_r :
  rngl_has_opp T = true →
  ∀ a b c, ((a - b ) × c = a × c - b × c)%L.

Theorem rngl_sub_mul_l_diag_r :
  rngl_has_opp T = true →
  ∀ a b : T, (a × b - b)%L = ((a - 1) × b)%L.

Theorem rngl_sub_mul_r_diag_r :
  rngl_has_opp T = true →
  ∀ a b, (a - b × a = (1 - b ) × a)%L.

Theorem rngl_mul_0_sub_1_comm :
  rngl_has_opp T = true →
  ∀ a, ((0 - 1) × a = a × (0 - 1))%L.

Theorem rngl_mul_if_then_else_distr : ∀ (x : bool) a b c d,
  ((if x then a else b ) × (if x then c else d ) =
    if x then a × c else b × d)%L.

Theorem rngl_characteristic_1 :
  rngl_has_opp_or_psub T = true →
  rngl_characteristic T = 1 →
  ∀ x, x = 0%L.

Theorem rngl_1_eq_0_iff :
  rngl_has_opp_or_psub T = true →
  rngl_characteristic T = 1 ↔ (1 = 0)%L.
Theorem rngl_mul_opp_opp :
  rngl_has_opp T = true →
  ∀ a b, (- a × - b = a × b)%L.

Theorem rngl_squ_opp_1 :
  rngl_has_opp T = true →
  (-1 × -1)%L = 1%L.

Theorem rngl_mul_nat_mul_nat_1 :
  rngl_has_opp_or_psub T = true →
  ∀ a n, rngl_mul_nat a n = (a × rngl_of_nat n)%L.

Theorem rngl_mul_nat_comm :
  rngl_has_opp_or_psub T = true →
  ∀ n a, (rngl_of_nat n × a = a × rngl_of_nat n)%L.

Theorem fold_rngl_of_nat :
  ∀ n, List.fold_right rngl_add 0%L (List.repeat 1 n)%L = rngl_of_nat n.

Theorem rngl_of_nat_mul :
  rngl_has_opp_or_psub T = true →
  ∀ m n : nat, rngl_of_nat (m × n) = (rngl_of_nat m × rngl_of_nat n)%L.

Theorem rngl_of_nat_inj :
  rngl_has_opp_or_psub T = true →
  ∀ i j,
  rngl_of_nat i = rngl_of_nat j
  → if Nat.eq_dec (rngl_characteristic T) 0 then i = j
    else i mod rngl_characteristic T = j mod rngl_characteristic T.

Theorem rngl_of_nat_pow :
  rngl_has_opp_or_psub T = true →
  ∀ a n, rngl_of_nat (a ^ n) = (rngl_of_nat a ^ n)%L.

Theorem rngl_mul_nat_pow_comm :
  rngl_has_opp_or_psub T = true →
  ∀ a b n, (rngl_of_nat a ^ n × b = b × rngl_of_nat a ^ n)%L.

Theorem rngl_pow_0_l :
  rngl_has_opp_or_psub T = true →
  ∀ n, (0 ^ n)%L = match n with 0 ⇒ 1%L | _ ⇒ 0%L end.

Theorem rngl_pow_0_r : ∀ a, (a ^ 0 = 1)%L.

Theorem rngl_pow_add_r : ∀ a i j, (a ^ (i + j ) = a ^ i × a ^ j)%L.

Theorem rngl_squ_opp :
  rngl_has_opp T = true →
  ∀ a, rngl_squ (- a)%L = rngl_squ a.

Theorem rngl_squ_add :
  rngl_mul_is_comm T = true →
  ∀ a b, (rngl_squ (a + b) = rngl_squ a + 2 × a × b + rngl_squ b)%L.

Theorem rngl_squ_sub :
  rngl_has_opp T = true →
  rngl_mul_is_comm T = true →
  ∀ a b, (rngl_squ (a - b) = rngl_squ a - 2 × a × b + rngl_squ b)%L.

Theorem rngl_squ_sub_comm :
  rngl_has_opp T = true →
  ∀ a b, ((a - b )² = (b - a )²)%L.

Theorem rngl_squ_mul :
  rngl_mul_is_comm T = true →
  ∀ a b, rngl_squ (a × b)%L = (rngl_squ a × rngl_squ b)%L.

Theorem rngl_pow_1_r : ∀ a, (a ^ 1)%L = a.

Theorem rngl_pow_succ_l : ∀ n a, (a ^ S n = a ^ n × a)%L.

Theorem rngl_pow_succ_r : ∀ n a, (a ^ S n = a × a ^ n)%L.

Theorem rngl_squ_0 :
  rngl_has_opp_or_psub T = true →
  (0² = 0)%L.

Theorem rngl_squ_1 : (1² = 1)%L.

Theorem rngl_squ_sub_squ :
  rngl_has_opp T = true →
  ∀ a b, (a ² - b ² = (a + b ) × (a - b ) + a × b - b × a)%L.

Theorem rngl_squ_sub_squ' :
  rngl_has_opp T = true →
  ∀ a b, ((a + b ) × (a - b ) = a ² - b ² + b × a - a × b)%L.

Theorem rngl_squ_pow_2 : ∀ a, (a ² = a ^ 2)%L.

Theorem rngl_pow_1_l : ∀ n, (1 ^ n = 1)%L.

Theorem rngl_pow_mul_l :
  rngl_mul_is_comm T = true →
  ∀ a b n, ((a × b ) ^ n = a ^ n × b ^ n)%L.

Theorem rngl_pow_mul_r : ∀ a m n, (a ^ (m × n ) = (a ^ m ) ^ n)%L.

Theorem rngl_pow_opp_1_even :
  rngl_has_opp T = true →
  ∀ n, ((-1) ^ (2 × n ) = 1)%L.

Theorem rngl_pow_opp_1_odd :
  rngl_has_opp T = true →
  ∀ n, ((-1) ^ S (2 × n) = -1)%L.

Theorem rngl_pow_squ : ∀ a n, ((a ^ n )² = a ^ (2 × n ))%L.

Theorem rngl_div_eq_inv_r :
  rngl_has_inv T = true →
  ∀ a b, (a / b)%L = (a × b⁻¹)%L.

Definition minus_one_pow n :=
  match n mod 2 with
  | 0 ⇒ 1%L
  | _ ⇒ (- 1%L)%L
  end.

Theorem minus_one_pow_succ :
  rngl_has_opp T = true →
  ∀ i, minus_one_pow (S i) = (- minus_one_pow i)%L.

Theorem minus_one_pow_add :
  rngl_has_opp T = true →
  ∀ a b, minus_one_pow (a + b) = (minus_one_pow a × minus_one_pow b)%L.

Theorem Brahmagupta_Fibonacci_identity :
  rngl_mul_is_comm T = true →
  rngl_has_opp T = true →
  ∀ a b c d,
  ((a ² + b ² ) × (c ² + d ² ) = (a × c - b × d )² + (a × d + b × c )²)%L.

Theorem Brahmagupta_Fibonacci_identity_2 :
  rngl_mul_is_comm T = true →
  rngl_has_opp T = true →
  ∀ a b c d,
  ((a ² + b ² ) × (c ² + d ² ) = (a × c + b × d )² + (a × d - b × c )²)%L.

End a.

Arguments rngl_characteristic_1 {T ro rp} Hos Hch x%_L.
Arguments rngl_mul_assoc {T ro rp} (a b c)%_L : rename.
Arguments rngl_mul_comm {T ro rp} Hic (a b)%_L.
Arguments rngl_mul_mul_swap {T ro rp} Hic (a b c)%_L.
Arguments rngl_mul_0_r {T ro rp} Hom a%_L.
Arguments rngl_mul_1_r {T ro rp} a%_L.
Arguments rngl_mul_2_l {T ro rp} a%_L.
Arguments rngl_pow_squ {T ro rp} a%_L n%_nat.

This page has been generated by coqdoc