mathlib documentation

Equations

• rat.denumerable = let T : Type := {x // 0 < x.snd ∧ x.fst.nat_abs.coprime x.snd}, _inst : infinite T := rat.denumerable._proof_1, _inst_1 : encodable T := encodable.subtype, _inst_2 : denumerable T := denumerable.of_encodable_of_infinite T in denumerable.of_equiv T denumerable_aux