Commit 2024-04-23 23:19 1a5d1288

View on Github →

feat: NNRat.cast (#11203) Define the canonical coercion from the nonnegative rationals to any division semiring. From LeanAPAP

Estimated changes

added def NNRat.castRec
added theorem NNRat.cast_def
added theorem NNRat.smul_def
added theorem NNRat.smul_one_eq_coe
modified theorem MulOpposite.op_ratCast
modified theorem MulOpposite.unop_ratCast
added theorem ULift.down_nnratCast
added theorem ULift.up_nnratCast
added theorem NNRat.cast_nonneg
added theorem Nonneg.coe_nnqsmul
added theorem Nonneg.coe_nnratCast
added theorem Nonneg.mk_nnqsmul
added theorem Nonneg.mk_nnratCast
added theorem nnqsmul_nonneg
added theorem star_nnratCast
added theorem Complex.im_nnratCast
added theorem Complex.ofReal_nnqsmul
added theorem Complex.re_nnratCast
modified theorem NNRat.coe_mk
modified theorem NNRat.coe_natCast
modified theorem NNRat.coe_one
modified theorem NNRat.coe_zero
added theorem NNRat.val_eq_cast
added theorem NNRat.cast_comm
added theorem NNRat.cast_commute
added theorem NNRat.cast_natCast
added theorem NNRat.cast_ofNat
added theorem NNRat.cast_one
added theorem NNRat.cast_zero
added theorem NNRat.commute_cast
added theorem eq_nnratCast
added theorem map_nnratCast
added theorem NNRat.cast_eq_id
added theorem NNRat.cast_id
added theorem Real.cauchy_nnratCast