ND0239

UnitProductFactor(m,i,v)

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

The independently decided weighted factor is i when Coprime(i,m), and one otherwise. It contains neither Phi nor Euler's conclusion.

Conservative notation; not a theorem, primitive, or axiom.

Definition in prerequisite notation

Coprime(i,m) ∧ v = i ∨ ¬Coprime(i,m) ∧ v = 1

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
(((forall eut_divisor_eu_bottomlayer_coprime. (exists eut_left_eu_bottomlayer_coprime. ((i)) = eut_divisor_eu_bottomlayer_coprime * eut_left_eu_bottomlayer_coprime) -> (exists eut_right_eu_bottomlayer_coprime. ((m)) = eut_divisor_eu_bottomlayer_coprime * eut_right_eu_bottomlayer_coprime) -> eut_divisor_eu_bottomlayer_coprime = 1) /\ ((v))=((i))) \/ (~(forall eut_divisor_eu_bottomlayer_coprime. (exists eut_left_eu_bottomlayer_coprime. ((i)) = eut_divisor_eu_bottomlayer_coprime * eut_left_eu_bottomlayer_coprime) -> (exists eut_right_eu_bottomlayer_coprime. ((m)) = eut_divisor_eu_bottomlayer_coprime * eut_right_eu_bottomlayer_coprime) -> eut_divisor_eu_bottomlayer_coprime = 1) /\ ((v))=1))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Coprime(a,b)

Definitions depending on this notation

UnitProductPrefix(m,b,c,l)

Checked theorems using this definition

EU000E · euler_unit_product_factor_existsEU000F · euler_unit_product_factor_unit_valueEU0010 · euler_unit_product_factor_nonunit_valueEU0011 · euler_unit_product_factor_coprimeEU0013 · euler_unit_product_prefix_extendEU0014 · euler_unit_product_prefix_existsEU0016 · euler_unit_product_prefix_entryEU0018 · euler_unit_factor_scaled_congruenceEU0019 · euler_nonunit_factor_unchanged_congruenceEU001B · euler_unit_product_reindex_scale