Finite Field
30秒診断
NPAへ戻る

Module

Mathlib.Algebra.Group.Subgroup.Order

npa-mathlib

Packages

2

Module

63

Theorem

750

Declarations

1016

信頼境界外の sidecar

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

Theorem

12

Definition

3

Inductive type

0

Axiom

0

Declarations

SubgroupLe

forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), Prop

definition

SubgroupEquiv

forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), Prop

definition

NormalContains

forall (G : Sort u), forall (N : forall (x : G), Prop), forall (H : forall (x : G), Prop), Prop

definition

subgroup_le_refl

forall (G : Sort u), forall (H : forall (x : G), Prop), @SubgroupLe.{u} G H H

theorem

subgroup_le_trans

forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (L : forall (x : G), Prop), forall (hk : @SubgroupLe.{u} G H K...

theorem

subgroup_equiv_intro

forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (hk : @SubgroupLe.{u} G H K), forall (kh : @SubgroupLe.{u} G K...

theorem

subgroup_equiv_left

forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (h_equiv_k : @SubgroupEquiv.{u} G H K), @SubgroupLe.{u} G H K

theorem

subgroup_equiv_right

forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (h_equiv_k : @SubgroupEquiv.{u} G H K), @SubgroupLe.{u} G K H

theorem

subgroup_equiv_refl

forall (G : Sort u), forall (H : forall (x : G), Prop), @SubgroupEquiv.{u} G H H

theorem

subgroup_equiv_symm

forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (h_equiv_k : @SubgroupEquiv.{u} G H K), @SubgroupEquiv.{u} G K...

theorem

subgroup_equiv_trans

forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (L : forall (x : G), Prop), forall (h_equiv_k : @SubgroupEquiv...

theorem

normal_contains_to_subgroup_le

forall (G : Sort u), forall (N : forall (x : G), Prop), forall (H : forall (x : G), Prop), forall (contains : @NormalContains.{u} G N H), @SubgroupLe.{u} G N H

theorem

subgroup_le_to_normal_contains

forall (G : Sort u), forall (N : forall (x : G), Prop), forall (H : forall (x : G), Prop), forall (le : @SubgroupLe.{u} G N H), @NormalContains.{u} G N H

theorem

normal_contains_refl

forall (G : Sort u), forall (N : forall (x : G), Prop), @NormalContains.{u} G N N

theorem

normal_contains_trans

forall (G : Sort u), forall (N : forall (x : G), Prop), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (nh : @NormalContains.{u} G...

theorem

Hashes

source
sha256:1d351d2165afb4ef7b4dbc3dba8c2f3a2cb30d8d35f90e15ed0cce5c6a8fdebc
certificateFile
sha256:5da33730332206a1debca756d4ff04fbd8fa1b3ea84cb15d92676652f7eb7613
export
sha256:e437fa6d0d71c25cfd931ece5572e3f232a08d7c9c8ece7c3ebf1cd4cf0beee6
axiomReport
sha256:3d3fdbf6a3ca4756ceaac9853e839a84878b24c0f6290e2246a78c6184b31e0e
certificate
sha256:c501393a7f67b539b33378767cd9a3f89205a604c902036c001aa1d6f4dd84f5

Source

import Std.Logic.Eq
import Mathlib.Logic.EqReasoning
import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Subgroup

def SubgroupLe.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), Prop :=
  fun G => fun H => fun K => forall (x : G), forall (hx : H x), K x

def SubgroupEquiv.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), Prop :=
  fun G => fun H => fun K => forall (P : Prop), forall (mk : forall (left : @SubgroupLe.{u} G H K), forall (right : @SubgroupLe.{u} G K H), P), P

def NormalContains.{u} :
  forall (G : Sort u), forall (N : forall (x : G), Prop), forall (H : forall (x : G), Prop), Prop :=
  fun G => fun N => fun H => forall (x : G), forall (hn : N x), H x

theorem subgroup_le_refl.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), @SubgroupLe.{u} G H H :=
  fun G => fun H => fun (x : G) => fun (hx : H x) => hx

theorem subgroup_le_trans.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (L : forall (x : G), Prop), forall (hk : @SubgroupLe.{u} G H K), forall (kl : @SubgroupLe.{u} G K L), @SubgroupLe.{u} G H L :=
  fun G => fun H => fun K => fun L => fun hk => fun kl => fun (x : G) => fun (hx : H x) => kl x (hk x hx)

theorem subgroup_equiv_intro.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (hk : @SubgroupLe.{u} G H K), forall (kh : @SubgroupLe.{u} G K H), @SubgroupEquiv.{u} G H K :=
  fun G => fun H => fun K => fun hk => fun kh => fun (P : Prop) => fun (mk : forall (left : @SubgroupLe.{u} G H K), forall (right : @SubgroupLe.{u} G K H), P) => mk hk kh

theorem subgroup_equiv_left.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (h_equiv_k : @SubgroupEquiv.{u} G H K), @SubgroupLe.{u} G H K :=
  fun G => fun H => fun K => fun h_equiv_k => h_equiv_k (@SubgroupLe.{u} G H K) (fun (hk : @SubgroupLe.{u} G H K) => fun (kh : @SubgroupLe.{u} G K H) => hk)

theorem subgroup_equiv_right.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (h_equiv_k : @SubgroupEquiv.{u} G H K), @SubgroupLe.{u} G K H :=
  fun G => fun H => fun K => fun h_equiv_k => h_equiv_k (@SubgroupLe.{u} G K H) (fun (hk : @SubgroupLe.{u} G H K) => fun (kh : @SubgroupLe.{u} G K H) => kh)

theorem subgroup_equiv_refl.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), @SubgroupEquiv.{u} G H H :=
  fun G => fun H => @subgroup_equiv_intro.{u} G H H (@subgroup_le_refl.{u} G H) (@subgroup_le_refl.{u} G H)

theorem subgroup_equiv_symm.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (h_equiv_k : @SubgroupEquiv.{u} G H K), @SubgroupEquiv.{u} G K H :=
  fun G => fun H => fun K => fun h_equiv_k => @subgroup_equiv_intro.{u} G K H (@subgroup_equiv_right.{u} G H K h_equiv_k) (@subgroup_equiv_left.{u} G H K h_equiv_k)

theorem subgroup_equiv_trans.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (L : forall (x : G), Prop), forall (h_equiv_k : @SubgroupEquiv.{u} G H K), forall (k_equiv_l : @SubgroupEquiv.{u} G K L), @SubgroupEquiv.{u} G H L :=
  fun G => fun H => fun K => fun L => fun h_equiv_k => fun k_equiv_l => @subgroup_equiv_intro.{u} G H L (@subgroup_le_trans.{u} G H K L (@subgroup_equiv_left.{u} G H K h_equiv_k) (@subgroup_equiv_left.{u} G K L k_equiv_l)) (@subgroup_le_trans.{u} G L K H (@subgroup_equiv_right.{u} G K L k_equiv_l) (@subgroup_equiv_right.{u} G H K h_equiv_k))

theorem normal_contains_to_subgroup_le.{u} :
  forall (G : Sort u), forall (N : forall (x : G), Prop), forall (H : forall (x : G), Prop), forall (contains : @NormalContains.{u} G N H), @SubgroupLe.{u} G N H :=
  fun G => fun N => fun H => fun contains => contains

theorem subgroup_le_to_normal_contains.{u} :
  forall (G : Sort u), forall (N : forall (x : G), Prop), forall (H : forall (x : G), Prop), forall (le : @SubgroupLe.{u} G N H), @NormalContains.{u} G N H :=
  fun G => fun N => fun H => fun le => le

theorem normal_contains_refl.{u} :
  forall (G : Sort u), forall (N : forall (x : G), Prop), @NormalContains.{u} G N N :=
  fun G => fun N => fun (x : G) => fun (hn : N x) => hn

theorem normal_contains_trans.{u} :
  forall (G : Sort u), forall (N : forall (x : G), Prop), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (nh : @NormalContains.{u} G N H), forall (hk : @NormalContains.{u} G H K), @NormalContains.{u} G N K :=
  fun G => fun N => fun H => fun K => fun nh => fun hk => fun (x : G) => fun (hn : N x) => hk x (nh x hn)