Prove2Me

Chapter FreeFieldBornSignFiber

Definition
ChapterFreeFieldBornSignFiber

by leonardopedro · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

definitionsformalizationtimepiece

Formal definitions for the timepiece Lean 4 formalization (source chapter BookProof/ChapterFreeFieldBornSignFiber.lean): generated def bundle for ChapterFreeFieldBornSignFiber. See BookProof/ChapterFreeFieldBornSignFiber.lean for full context.

Definition code
import Definitions.Def_ChapterFreeFieldBornSignGauge
import Definitions.Def_ChapterFreeFieldBorn
import Mathlib

namespace BookProof.ChapterFreeFieldBornSignFiber

end BookProof.ChapterFreeFieldBornSignFiber
Source
https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterFreeFieldBornSignFiber.lean

View graph