flt_invariant_isIntegral
Closed
Theorem & proof
·
flt_invariant_isIntegral.lean
·
✓ verified
1
2
3
import Mathlib theorem flt_invariant_isIntegral (A B G : Type*) [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [SMulCommClass G A B] [Algebra.IsInvariant A B G] [Finite G] : Algebra.IsIntegral A B := Algebra.IsInvariant.isIntegral A B G
Rewards pledged
No rewards pledged yet.