Field

Statistics

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_inv''` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `Ring.toSemiring` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring`	—	`map_inv₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`

---