Jon Eugster f636a8d833 fix missing lemma docs from statement names

2023-04-03 11:53:48 +02:00

..

L01_Module.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

L02_VectorNotation.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

L03_VectorNotation.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

L04_Submodule.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

L05_Submodule.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

L06_Span.lean

fix missing lemma docs from statement names

2023-04-03 11:53:48 +02:00

L07_Span.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

L08_GeneratingSet.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

M01_LinearMap.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

M02_LinearIndep.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

M04_Basis.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

N01_Span.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

N02_Span.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

N03_Idempotent.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

N04_Idempotent.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

N05_Sum.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

N06_Sum.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

N07_Prod.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

N08_Prod.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00

N09_Prod.lean

rename testgame to adam, part 2

2023-03-23 17:10:44 +01:00