Algebra.PhiRing
IndisputableMonolith.Algebra.PhiRing
No prose has been written for this declaration yet. The Lean source and graph data below render without it.
generate prose now
From the project-wide theorem graph. These declarations reference this one in their body.
IndisputableMonolith.Algebra.RecognitionCategory
Lean names referenced from this declaration's body.
IndisputableMonolith.Algebra.CostAlgebra
IndisputableMonolith.Cost
sqrt5_pos
phi_pos
phi_gt_one
phi_equation
psi_equation
phi_psi_product
phi_psi_sum
phi_psi_diff
phi_inv
PhiInt
phiPow
phiInt_sq
J_at_phi
phi_ring_certificate