HepLean Documentation

Mathlib.Data.Rat.Encodable

The rationals are Encodable. #

As a consequence we also get the instance Countable.

This is kept separate from Data.Rat.Defs in order to minimize imports.

Equations
  • One or more equations did not get rendered due to their size.