inductive
definition
ComplexTheoremRS
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.ComplexAnalysisFromRS on GitHub at line 22.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
19
20namespace IndisputableMonolith.Mathematics.ComplexAnalysisFromRS
21
22inductive ComplexTheoremRS where
23 | cauchy | residue | riemannMapping | liouville | maximumModulus
24 deriving DecidableEq, Repr, BEq, Fintype
25
26theorem complexTheoremCount : Fintype.card ComplexTheoremRS = 5 := by decide
27
28/-- Complex plane dimension = D-1 = 2. -/
29def complexDim : ℕ := 2
30theorem complexDim_eq_Dm1 : complexDim = 3 - 1 := by decide
31
32structure ComplexAnalysisCert where
33 five_theorems : Fintype.card ComplexTheoremRS = 5
34 complex_dim : complexDim = 3 - 1
35
36def complexAnalysisCert : ComplexAnalysisCert where
37 five_theorems := complexTheoremCount
38 complex_dim := complexDim_eq_Dm1
39
40end IndisputableMonolith.Mathematics.ComplexAnalysisFromRS