module
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RationalField
show as:
view Lean formalization →
used by (3)
depends on (1)
declarations in this module (31)
-
def
positive -
theorem
positive_iff_toRat_pos -
theorem
positive_normalize -
theorem
positive_not_zero -
def
div -
instance
instDiv -
theorem
div_eq -
theorem
toRat_div -
theorem
positive_ne_zero -
theorem
add_assoc' -
theorem
zero_add' -
theorem
add_zero' -
theorem
add_left_neg' -
theorem
add_right_neg' -
theorem
mul_assoc' -
theorem
one_mul' -
theorem
mul_one' -
theorem
zero_mul' -
theorem
mul_zero' -
theorem
right_distrib' -
theorem
left_distrib' -
theorem
inv_zero -
theorem
inv_mul_cancel -
theorem
div_mul_cancel -
theorem
mul_div_cancel -
def
onPRCRat -
theorem
onPRCRat_mk -
theorem
onPRCRat_toRat -
theorem
onPRCRat_normalized_representative -
structure
RationalFieldCertificate -
theorem
rational_field_certificate