Lifting groups with zero along injective/surjective maps #
Pullback a MulZeroClass
instance along an injective function.
See note [reducible non-instances].
Equations
- Function.Injective.mulZeroClass f hf zero mul = MulZeroClass.mk (_ : ∀ (a : M₀'), 0 * a = 0) (_ : ∀ (a : M₀'), a * 0 = 0)
Pushforward a MulZeroClass
instance along an surjective function.
See note [reducible non-instances].
Equations
- Function.Surjective.mulZeroClass f hf zero mul = MulZeroClass.mk (_ : ∀ (y : M₀'), 0 * y = 0) (_ : ∀ (y : M₀'), y * 0 = 0)
Pushforward a NoZeroDivisors
instance along an injective function.
Pullback a MulZeroOneClass
instance along an injective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Pushforward a MulZeroOneClass
instance along an surjective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Pullback a SemigroupWithZero
along an injective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Pushforward a SemigroupWithZero
along an surjective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Pullback a MonoidWithZero
along an injective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Pushforward a MonoidWithZero
along a surjective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Pullback a CommMonoidWithZero
along an injective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Pushforward a CommMonoidWithZero
along a surjective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Pullback a CancelMonoidWithZero
along an injective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Pullback a CancelCommMonoidWithZero
along an injective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Pullback a GroupWithZero
along an injective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Pushforward a GroupWithZero
along an surjective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Pullback a CommGroupWithZero
along an injective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Pushforward a CommGroupWithZero
along a surjective function.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.