lemma
proved
term proof
one
show as:
view Lean formalization →
formal statement (Lean)
71lemma one (φ : ℝ) : PhiClosed φ (1 : ℝ) :=
proof body
Term-mode proof.
72 (phiSubfield φ).one_mem
73
used by (40)
-
costRateEL_implies_const_one -
geodesicEquationHolds -
actionJ_convex_on_interp -
actionJ_local_min_is_global -
actionJ_minimum_unique_value -
no_eighth_plot -
Jcost_anti_mono_on_unit_interval -
symmetryGroupPreferenceCert -
canonicalRecognitionCostSystem_cost_inv -
shiftedCompose_val -
windowSums -
PhiInt -
PhiInt -
phiInt_sq -
phi_ring_certificate -
canonicalPhiRingObj -
initial_morphism_exists -
phiRing_comp -
PhiRingHom -
PhiRingObj -
trivial -
eV_to_J_pos -
rs_pattern -
ml_nucleosynthesis_eq_phi -
NuclearTier -
r_orbit_adjacent_ratio_band -
bimodal_ratio_lt_phi_nine -
ml_is_phi_power -
fr_valence_one -
essentialSymmetry