Exact

Statistics

Name	Kind	Assumes	Proves	Validates	Depends On
`map_exact` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Module.toDistribMulAction` `map`	—	`Function.Exact.of_ladder_linearEquiv_of_exact` `IsScalarTower.left` `IsScalarTower.right` `smulCommClass_self` `localizedModuleIsLocalizedModule` `map_iso_commute` `LocalizedModule.map_exact`

Name	Kind	Assumes	Proves	Validates	Depends On
`map_exact` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`LocalizedModule` `OreLocalization.instAddCommMonoidOreLocalization` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `Module.toDistribMulAction` `OreLocalization.instModuleOfIsScalarTower` `Semiring.toModule` `IsScalarTower.left` `DistribMulAction.toMulAction` `IsScalarTower.right` `Algebra.id` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommMonoid.toMonoid` `IsLocalizedModule.map` `mkLinearMap` `localizedModuleIsLocalizedModule` `OreLocalization.instZero`	—	`IsScalarTower.left` `IsScalarTower.right` `smulCommClass_self` `localizedModuleIsLocalizedModule` `induction_on` `smul_zero` `one_smul` `mk_eq` `IsLocalizedModule.map_LocalizedModules` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Submonoid.mk_smul` `mk_cancel_common_left`

---