IsIntegrallyClosed.of_isIntegrallyClosedIn_of_faithfulSMul
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_of_isIntegrallyClosedIn_of_faithfulSMulLean source · statement
theorem _root_.IsIntegrallyClosed.of_isIntegrallyClosedIn_of_faithfulSMul
(A F : Type*) [CommRing A] [IsDomain A] [Field F] [Algebra A F] [FaithfulSMul A F]
[IsIntegrallyClosedIn A F] : IsIntegrallyClosed A