Theorems · Definition · functional analysis

NormedRing.recOn

{α : Type u_5} →
  {motive : NormedRing α → Sort u} →
    (t : NormedRing α) →
      ([toNorm : Norm α] →
          [toRing : Ring α] →
            [toMetricSpace : MetricSpace α] →
              (dist_eq : ∀ (x y : α), dist x y = ‖-x + y‖) →
                (norm_mul_le : ∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖) →
                  motive
                    { toNorm := toNorm, toRing := toRing, toMetricSpace := toMetricSpace, dist_eq := dist_eq,
                      norm_mul_le := norm_mul_le }) →
        motive t

Defined in

Mathlib.Analysis.Normed.Ring.Basic

Cited by

0 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound