module
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.ChartTransition
show as:
view Lean formalization →
used by (1)
depends on (1)
declarations in this module (13)
-
structure
FactorPair -
def
factorPairProduct -
def
archimedeanMagnitude -
theorem
factorPairProduct_toNat -
theorem
same_product_same_magnitude -
theorem
two_six_product_eq_three_four -
theorem
two_ne_three -
theorem
six_ne_four -
theorem
magnitude_underdetermines_left_factor -
theorem
magnitude_underdetermines_right_factor -
theorem
nontrivialFactorization_of_proper_divisor -
structure
ChartTransitionCertificate -
theorem
chart_transition_certificate