Theorems · Definition · functional analysis

AlgebraNorm.noConfusion

{P : Sort u} →
  {R : Type u_1} →
    {inst : SeminormedCommRing R} →
      {S : Type u_2} →
        {inst_1 : Ring S} →
          {inst_2 : Algebra R S} →
            {t : AlgebraNorm R S} →
              {R' : Type u_1} →
                {inst' : SeminormedCommRing R'} →
                  {S' : Type u_2} →
                    {inst'_1 : Ring S'} →
                      {inst'_2 : Algebra R' S'} →
                        {t' : AlgebraNorm R' S'} →
                          R = R' →
                            inst ≍ inst' →
                              S = S' → inst_1 ≍ inst'_1 → inst_2 ≍ inst'_2 → t ≍ t' → AlgebraNorm.noConfusionType P t t'

Defined in

Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Cited by

0 results in Mathlib

Foundations

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