instance Units.instInvFloat_leanUnits : Inv Float

Equations

• Units.instInvFloat_leanUnits = { inv := fun (v : Float) => 1.0 / v }

instance Units.instPowFloatNat_leanUnits : Pow Float Nat

Equations

• Units.instPowFloatNat_leanUnits = { pow := fun (v : Float) (n : Nat) => v ^ Float.ofNat n }

instance Units.instPowFloatInt_leanUnits : Pow Float Int

Equations

• Units.instPowFloatInt_leanUnits = { pow := fun (v : Float) (n : Int) => v ^ Float.ofInt n }

instance Units.instPowFloatRat_leanUnits : Pow Float Rat

Equations

• Units.instPowFloatRat_leanUnits = { pow := fun (v : Float) (n : Rat) => v.pow (Float.ofInt n.num / Float.ofNat n.den) }

instance Units.instRatCastFloat_leanUnits : RatCast Float

Equations

• Units.instRatCastFloat_leanUnits = { ratCast := fun (q : Rat) => q.toFloat }