Commit 2023-03-06 10:01 b55832c6

View on Github →

feat: port Topology.Instances.Rat (#2643)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Instances/Rat.lean

added theorem Int.closedEmbedding_coe_rat

added theorem Int.dist_cast_rat

added theorem Int.uniformEmbedding_coe_rat

added theorem Nat.closedEmbedding_coe_rat

added theorem Nat.dist_cast_rat

added theorem Nat.uniformEmbedding_coe_rat

added theorem Rat.continuous_coe_real

added theorem Rat.denseEmbedding_coe_real

added theorem Rat.dist_cast

added theorem Rat.dist_eq

added theorem Rat.embedding_coe_real

added theorem Rat.uniformContinuous_abs

added theorem Rat.uniformContinuous_add

added theorem Rat.uniformContinuous_coe_real

added theorem Rat.uniformContinuous_neg

added theorem Rat.uniformEmbedding_coe_real