Hyperfields/Fields/Hyperphysics.lean

Explanation legend

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

1 declarations, 0 contain sorry, 0 axioms

Hyperphysics

This module gives Hyperphysics a first-class page in the unified Hyperfields explainer. The complete source-pinned description and review state live in the registry entry referenced below.

Imports (1)
Imported by 1 file
  1. def Hyperfields.Fields.Hyperphysics.entry Hyperphysics explainer entry line 17 source

    The canonical Hyperphysics record used by the unified portal.

    This declaration exposes the checked ecosystem record for Hyperphysics on its own stable explainer page.

    See also: Hyperfields.hyperphysics

    standard axioms: propext what this means

    Statement uses: Hyperfields.Entry

    Proof uses: Hyperfields.hyperphysics

    def entry : Hyperfields.Entry := Hyperfields.hyperphysics
    …

    Mentions: Hyperfields.Entry, Hyperfields.hyperphysics