theorem
proved
agObjectCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.AlgebraicGeometryFromRS on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
25 | affineVariety | projectiveVariety | calabiYau | K3Surface | ellipticCurve
26 deriving DecidableEq, Repr, BEq, Fintype
27
28theorem agObjectCount : Fintype.card AlgebraicGeometryObject = 5 := by decide
29
30/-- Calabi-Yau threefold dimension = D = 3. -/
31def cyDimension : ℕ := 3
32theorem cyDimension_eq_D : cyDimension = 3 := rfl
33
34structure AlgebraicGeometryCert where
35 five_objects : Fintype.card AlgebraicGeometryObject = 5
36 cy_dim : cyDimension = 3
37
38def algebraicGeometryCert : AlgebraicGeometryCert where
39 five_objects := agObjectCount
40 cy_dim := cyDimension_eq_D
41
42end IndisputableMonolith.Mathematics.AlgebraicGeometryFromRS