Simple-module counts under algebra equivalence

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.simpleCount_mapAlgEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (f : A ≃ₐ[k] B) : (S.mapAlgEquiv f).simpleCount = S.simpleCount

Transporting the complete family along an algebra equivalence preserves the literal number of simple-module classes.