Documentation

LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One

Imports

Init
Mathlib.Tactic.NormNum.Abs
Mathlib.Tactic.NormNum.DivMod
Mathlib.Tactic.NormNum.OfScientific
Mathlib.Tactic.NormNum.Pow
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One.Lift
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One.PreLift
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One.Strat
Mathlib.Data.Rat.Cast.Order

Imported by

Player one proof index #

Import-only index for the player-one lift and strategy construction modules.