Documentation Verification Report

Flat

📁 Source: Mathlib/RingTheory/Smooth/Flat.lean

Statistics

Metric	Count
Definitions `Flat`, `Flat`	2
Theorems `flat_of_algHom_of_isNoetherianRing`, `flat`, `flat_of_isNoetherianRing`, `flat`	4
Total	6

Algebra.FormallySmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flat_of_algHom_of_isNoetherianRing` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	`Module.Flat` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `IsScalarTower.right` `Module.Flat.trans` `AdicCompletion.instIsScalarTower` `AdicCompletion.flat_of_isNoetherian` `exists_kerProj_comp_eq_id` `Module.Flat.of_retract` `LinearMap.ext` `RingHomCompTriple.ids`

Algebra.Smooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flat` 📖	mathematical	—	`Module.Flat` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring`	—	`Algebra.to_smulCommClass` `exists_finiteType` `Algebra.FiniteType.isNoetherianRing` `isNoetherian_of_isNoetherianRing_of_finite` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `AddGroup.instFGInt` `flat_of_isNoetherianRing` `Module.Flat.of_linearEquiv` `Module.Flat.baseChange`
`flat_of_isNoetherianRing` 📖	mathematical	—	`Module.Flat` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `CommSemiring.toSemiring`	—	`Algebra.FiniteType.iff_quotient_mvPolynomial''` `Algebra.FiniteType.of_finitePresentation` `finitePresentation` `Algebra.FormallySmooth.flat_of_algHom_of_isNoetherianRing` `Module.Flat.of_free` `MvPolynomial.instFree` `MvPolynomial.isNoetherianRing` `Finite.of_fintype` `formallySmooth`

ConvexCone

Definitions

Name	Category	Theorems
`Flat` 📖	MathDef	1 math math: `salient_iff_not_flat`

Module

Definitions

Name	Category	Theorems
`Flat` 📖	CompData	75 math math: `Flat.of_projective`, `Flat.iff_lTensor_exact'`, `Flat.iff_rTensor_preserves_injective_linearMap`, `Flat.of_free`, `Flat.localizedModule`, `Flat.finsupp`, `Algebra.Smooth.flat`, `faithfullyFlat_iff`, `FaithfullyFlat.iff_zero_iff_rTensor_zero`, `Flat.of_forall_exists_factorization`, `Flat.iff_lTensor_preserves_injective_linearMap`, `Flat.iff_rTensor_injective`, `Flat.iff_rTensor_preserves_shortComplex_exact`, `Flat.iff_lTensor_preserves_shortComplex_exact`, `Algebra.FormallySmooth.flat_of_algHom_of_isNoetherianRing`, `Flat.iff_lTensor_exact`, `Flat.iff_lTensor_preserves_injective_linearMap'`, `FaithfullyFlat.iff_zero_iff_lTensor_zero`, `FaithfullyFlat.iff_flat_and_ideal_smul_eq_top`, `Flat.dfinsupp_iff`, `Flat.instTensorProduct`, `Flat.instSubalgebraToSubmodule`, `Flat.of_flat_tensorProduct`, `Flat.instOfIsDedekindDomainOfIsTorsionFree`, `Flat.iff_lTensor_injective`, `FaithfullyFlat.iff_flat_and_lTensor_reflects_triviality`, `Flat.flat_iff_torsion_eq_bot_of_valuationRing_localization_isMaximal`, `Flat.iff_rTensor_exact'`, `Flat.iff_lTensor_injectiveₛ`, `Flat.baseChange`, `instFlatAtPrime`, `Flat.iff_rTensor_exact`, `Flat.flat_iff_torsion_eq_bot_of_isBezout`, `Algebra.FormallyUnramified.flat_of_restrictScalars`, `Flat.self`, `Flat.iff_forall_exists_factorization`, `Flat.iff_lTensor_preserves_injective_linearMapₛ`, `Flat.of_retract`, `Flat.shrink`, `Flat.trans`, `Flat.iff_lift_lsmul_comp_subtype_injective`, `Flat.instSubtypeMemSubmoduleSubmoduleAlgebra`, `Flat.iff_rTensor_preserves_injective_linearMapₛ`, `Flat.iff_preservesFiniteLimits_tensorLeft`, `Flat.iff_forall_isTrivialRelation`, `Flat.isBaseChange`, `Flat.of_linearEquiv`, `IsLocalization.flat`, `Flat.iff_flat_tensorProduct`, `RingHom.flat_algebraMap_iff`, `Flat.iff_rTensor_injectiveₛ`, `FaithfullyFlat.iff_flat_and_rTensor_faithful`, `Flat.of_isLocalizedModule`, `Flat.ulift`, `Flat.of_ulift`, `flat_iff`, `Flat.tfae_equational_criterion`, `Algebra.Smooth.flat_of_isNoetherianRing`, `Localization.flat`, `Flat.of_forall_isTrivialRelation`, `Flat.of_shrink`, `Flat.iff_rTensor_preserves_injective_linearMap'`, `FaithfullyFlat.iff_flat_and_lTensor_faithful`, `Flat.iff_rTensor_injective'`, `AdicCompletion.flat_of_isNoetherian`, `Flat.directSum_iff`, `Flat.iff_lTensor_injective'`, `FaithfullyFlat.iff_flat_and_proper_ideal`, `Flat.iff_characterModule_baer`, `FaithfullyFlat.toFlat`, `Flat.equiv_iff`, `Flat.iff_characterModule_injective`, `IsDedekindDomain.flat_iff_torsion_eq_bot`, `flat_iff_of_isLocalization`, `FaithfullyFlat.iff_flat_and_rTensor_reflects_triviality`

RingHom.Smooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flat` 📖	mathematical	—	`RingHom.Flat`	—	`Algebra.Smooth.flat` `toAlgebra`

---

← Back to Index