Basic

📁 Source: Sudoku4/Basic.lean

Statistics

Metric	Count
Definitions Grid, Extends, ofRArray, Rules, Standard, Eliminated, Eliminate₁, Looking, Solvable, num_vec, test1, «binderPred≤ᵍ_», «termMake_grid%[_,,]», «term_≤ᵍ_»	14
Theorems of_bne, ext, ext_iff, finish, step, box, box', column, row, self, ne, elim, intro, solvable, solvable_test1	15
Total	29

Sudoku

Definitions

Name	Category	Theorems
Grid 📖	CompOp	1 math math: Solvable.solvable
Rules 📖	CompOp	—
Solvable 📖	CompData	2 math math: solvable_test1, Solvable.intro
num_vec 📖	CompOp	—
test1 📖	CompOp	1 math math: solvable_test1
«binderPred≤ᵍ_» 📖	CompOp	—
«termMake_grid%[_,,]» 📖	CompOp	—
«term_≤ᵍ_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
solvable_test1 📖	mathematical	—	Solvable test1 Rules.Standard	—	Solvable.intro Grid.Extends.of_bne Rules.Standard.elim Rules.Standard.Eliminated.step Rules.Standard.Eliminate₁.row Rules.Standard.Eliminate₁.column Rules.Standard.Eliminate₁.box Rules.Standard.Eliminate₁.self Rules.Standard.Eliminated.finish Grid.ext Fin.cases' Fin.CheckFrom.step Fin.CheckFrom.last

Sudoku.Grid

Definitions

Name	Category	Theorems
Extends 📖	MathDef	1 math math: Sudoku.Solvable.solvable
ofRArray 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	—	—	—	—
ext_iff 📖	—	—	—	—	ext

Sudoku.Grid.Extends

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_bne 📖	—	Sudoku.Grid.Extends	—	—	—

Sudoku.Rules

Definitions

Name	Category	Theorems
Standard 📖	CompOp	1 math math: Sudoku.solvable_test1

Sudoku.Rules.Standard

Definitions

Name	Category	Theorems
Eliminated 📖	MathDef	1 math math: Eliminated.finish
Eliminate₁ 📖	MathDef	5 math math: Eliminate₁.box, Eliminate₁.row, Eliminate₁.column, Eliminate₁.self, Eliminate₁.box'
Looking 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
elim 📖	—	Sudoku.Rules.Standard Eliminated	—	—	Looking.ne

Sudoku.Rules.Standard.Eliminated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finish 📖	mathematical	—	Sudoku.Rules.Standard.Eliminated	—	—
step 📖	—	Sudoku.Rules.Standard.Eliminate₁ Sudoku.Rules.Standard.Eliminated	—	—	—

Sudoku.Rules.Standard.Eliminate₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
box 📖	mathematical	—	Sudoku.Rules.Standard.Eliminate₁	—	—
box' 📖	mathematical	—	Sudoku.Rules.Standard.Eliminate₁	—	—
column 📖	mathematical	—	Sudoku.Rules.Standard.Eliminate₁	—	—
row 📖	mathematical	—	Sudoku.Rules.Standard.Eliminate₁	—	—
self 📖	mathematical	—	Sudoku.Rules.Standard.Eliminate₁	—	—

Sudoku.Rules.Standard.Looking

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ne 📖	—	Sudoku.Rules.Standard Sudoku.Rules.Standard.Looking	—	—	—

Sudoku.Solvable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intro 📖	mathematical	Sudoku.Grid.Extends	Sudoku.Solvable	—	—
solvable 📖	mathematical	Sudoku.Solvable	Sudoku.Grid Sudoku.Grid.Extends	—	—

---

← Back to Index