module module

`IndisputableMonolith.RRF.Models.Trivial`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.RRF.Models module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.RRF.Core module_import

declarations in this module (15)

abbrev TrivialState L24
def trivialStrain L27
theorem trivial_balanced L34
theorem trivial_is_minimizer L37
def trivialLedger L41
theorem trivial_ledger_closed L46
def trivialStrainLedger L49
theorem trivial_is_valid L54
def trivialChannel L58
def trivialChannelBundle L63
def trivialOctave L69
theorem trivialOctave_wellPosed L76
theorem trivialModel_consistent L80
def trivialVantageTriple L85
theorem trivialVantageTriple_unified L88