Documentation Verification Report

Symbols

📁 Source: Mathlib/Algebra/FreeMonoid/Symbols.lean

Statistics

Metric	Count
Definitions `Symbols`, `symbols`, `symbols`	3
Theorems `mem_symbols`, `symbols_add`, `symbols_of`, `symbols_zero`, `mem_symbols`, `symbols_mul`, `symbols_of`, `symbols_one`	8
Total	11

FirstOrder.Language

Definitions

Name	Category	Theorems
`Symbols` 📖	CompOp	5 math math: `isEmpty_empty`, `empty.isFraisseLimit_of_countable_infinite`, `BoundedFormula.instCountableSymbolsWithConstants`, `isFraisseLimit_of_countable_nonempty_dlo`, `BoundedFormula.instCountableSymbolsConstantsOn`

FreeAddMonoid

Definitions

Name	Category	Theorems
`symbols` 📖	CompOp	4 math math: `symbols_of`, `symbols_zero`, `mem_symbols`, `symbols_add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_symbols` 📖	mathematical	—	`Finset` `Finset.instMembership` `symbols` `FreeAddMonoid` `instMembership`	—	`List.mem_toFinset`
`symbols_add` 📖	mathematical	—	`symbols` `FreeAddMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid` `instAddCancelMonoid` `Finset` `Finset.instUnion`	—	`List.toFinset_append`
`symbols_of` 📖	mathematical	—	`symbols` `of` `Finset` `Finset.instSingleton`	—	—
`symbols_zero` 📖	mathematical	—	`symbols` `FreeAddMonoid` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid` `instAddCancelMonoid` `Finset` `Finset.instEmptyCollection`	—	—

FreeMonoid

Definitions

Name	Category	Theorems
`symbols` 📖	CompOp	4 math math: `mem_symbols`, `symbols_of`, `symbols_one`, `symbols_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_symbols` 📖	mathematical	—	`Finset` `Finset.instMembership` `symbols` `FreeMonoid` `instMembership`	—	`List.mem_toFinset`
`symbols_mul` 📖	mathematical	—	`symbols` `FreeMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `instCancelMonoid` `Finset` `Finset.instUnion`	—	`List.toFinset_append`
`symbols_of` 📖	mathematical	—	`symbols` `of` `Finset` `Finset.instSingleton`	—	—
`symbols_one` 📖	mathematical	—	`symbols` `FreeMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `RightCancelMonoid.toMonoid` `CancelMonoid.toRightCancelMonoid` `instCancelMonoid` `Finset` `Finset.instEmptyCollection`	—	—

---

← Back to Index