Finite Field
30秒診断
NPAへ戻る

Module

Mathlib.Algebra.OrderedField

npa-mathlib

Packages

2

Module

63

Theorem

750

Declarations

1016

信頼境界外の sidecar

Source text や表示 overlay は提示用メタデータです。信頼する証拠は署名済み証明書と checker の結果です。

Theorem

9

Definition

3

Inductive type

0

Axiom

0

Declarations

le

forall (a : RingElem), forall (b : RingElem), Prop

definition

lt

forall (a : RingElem), forall (b : RingElem), Prop

definition

sqrt

forall (a : RingElem), RingElem

definition

le_refl

forall (a : RingElem), le a a

theorem

le_trans

forall (a : RingElem), forall (b : RingElem), forall (c : RingElem), forall (hab : le a b), forall (hbc : le b c), le a c

theorem

add_nonneg

forall (a : RingElem), forall (b : RingElem), forall (ha : le zero a), forall (hb : le zero b), le zero (add a b)

theorem

mul_nonneg

forall (a : RingElem), forall (b : RingElem), forall (ha : le zero a), forall (hb : le zero b), le zero (mul a b)

theorem

le_square_nonneg

forall (a : RingElem), le zero (sq a)

theorem

sqrt_nonneg

forall (a : RingElem), le zero (sqrt a)

theorem

sqrt_square_of_nonneg

forall (a : RingElem), forall (ha : le zero a), @Eq.{1} RingElem (sqrt (sq a)) a

theorem

sqrt_mul_self

forall (a : RingElem), forall (ha : le zero a), @Eq.{1} RingElem (sqrt (mul a a)) a

theorem

eq_of_square_eq_square_nonneg

forall (a : RingElem), forall (b : RingElem), forall (ha : le zero a), forall (hb : le zero b), forall (hsq : @Eq.{1} RingElem (sq a) (sq b)), @Eq.{1} RingElem...

theorem

Hashes

source
sha256:38b9b897053e42b44d734ad16f55b22e0671b7b01cd2e94e26e2a1ba9cf77b68
certificateFile
sha256:2015b97b9573a9c926a9a7f190d1f9c5d261048dfdde4c6aeeec899e4a09fc42
export
sha256:d6b08e865fb570cb11e57e903463edcd77f6f821126d9375dde24d73055ebf3f
axiomReport
sha256:7715c06c634de0020345067c58ecf3bd23c10e71d84f4b97cd4c2e00e82c1a07
certificate
sha256:111e0cb6227f6f80201a307469ec4a866f094a42a68dd49e7c4d092bfba5559a

Source

import Std.Logic.Eq
import Mathlib.Algebra.Ring
import Mathlib.Algebra.Square

def le :
  forall (a : RingElem), forall (b : RingElem), Prop :=
  fun a => fun b => @Eq.{1} RingElem RingElem.unit RingElem.unit

def lt :
  forall (a : RingElem), forall (b : RingElem), Prop :=
  fun a => fun b => @Eq.{1} RingElem RingElem.unit RingElem.unit

def sqrt :
  forall (a : RingElem), RingElem :=
  fun a => a

theorem le_refl :
  forall (a : RingElem), le a a :=
  fun a => @Eq.refl.{1} RingElem RingElem.unit

theorem le_trans :
  forall (a : RingElem), forall (b : RingElem), forall (c : RingElem), forall (hab : le a b), forall (hbc : le b c), le a c :=
  fun a => fun b => fun c => fun hab => fun hbc => @Eq.refl.{1} RingElem RingElem.unit

theorem add_nonneg :
  forall (a : RingElem), forall (b : RingElem), forall (ha : le zero a), forall (hb : le zero b), le zero (add a b) :=
  fun a => fun b => fun ha => fun hb => @Eq.refl.{1} RingElem RingElem.unit

theorem mul_nonneg :
  forall (a : RingElem), forall (b : RingElem), forall (ha : le zero a), forall (hb : le zero b), le zero (mul a b) :=
  fun a => fun b => fun ha => fun hb => @Eq.refl.{1} RingElem RingElem.unit

theorem le_square_nonneg :
  forall (a : RingElem), le zero (sq a) :=
  fun a => @Eq.refl.{1} RingElem RingElem.unit

theorem sqrt_nonneg :
  forall (a : RingElem), le zero (sqrt a) :=
  fun a => @Eq.refl.{1} RingElem RingElem.unit

theorem sqrt_square_of_nonneg :
  forall (a : RingElem), forall (ha : le zero a), @Eq.{1} RingElem (sqrt (sq a)) a :=
  fun a => fun ha => @RingElem.rec.{0} (fun (x : RingElem) => @Eq.{1} RingElem RingElem.unit x) (@Eq.refl.{1} RingElem RingElem.unit) a

theorem sqrt_mul_self :
  forall (a : RingElem), forall (ha : le zero a), @Eq.{1} RingElem (sqrt (mul a a)) a :=
  fun a => fun ha => @RingElem.rec.{0} (fun (x : RingElem) => @Eq.{1} RingElem RingElem.unit x) (@Eq.refl.{1} RingElem RingElem.unit) a

theorem eq_of_square_eq_square_nonneg :
  forall (a : RingElem), forall (b : RingElem), forall (ha : le zero a), forall (hb : le zero b), forall (hsq : @Eq.{1} RingElem (sq a) (sq b)), @Eq.{1} RingElem a b :=
  fun a => fun b => fun ha => fun hb => fun hsq => @RingElem.rec.{0} (fun (x : RingElem) => @Eq.{1} RingElem x b) (@RingElem.rec.{0} (fun (y : RingElem) => @Eq.{1} RingElem RingElem.unit y) (@Eq.refl.{1} RingElem RingElem.unit) b) a