Theorem A in the independent vocabulary

The Mathlib-only notions of Statement.lean agree with those of the proof library, so theoremA gives Statement.TheoremA.

theorem MultiplicativeBasisDeformations.Statement.isRepresentationFinite_of (k A : Type u) [Field k] [Ring A] [Algebra k A] (h : IsRepresentationFinite k A) : MultiplicativeBasisDeformations.IsRepresentationFinite k A

An independent complete family gives representation-finiteness in the sense of the proof library.

theorem MultiplicativeBasisDeformations.Statement.hasNormedMultiplicativeBasis_of (k A : Type u) [Field k] [Ring A] [Algebra k A] (h : MultiplicativeBasisDeformations.HasNormedMultiplicativeBasis k A) : HasNormedMultiplicativeBasis k A

A normed multiplicative basis of the proof library is one in the independent sense.

theorem MultiplicativeBasisDeformations.Statement.theoremA (k A : Type u) [Field k] [Ring A] [Algebra k A] [IsAlgClosed k] [FiniteDimensional k A] : TheoremA k A

Theorem A in the independent vocabulary.