Lifting groups with zero along injective/surjective maps

ink

def Function.Injective.mulZeroClass {M₀ : Type u_1} {M₀' : Type u_2} [inst : MulZeroClass M₀] [inst : Mul M₀'] [inst : Zero M₀'] (f : M₀' → M₀) (hf : Function.Injective f) (zero : f 0 = 0) (mul : ∀ (a b : M₀'), f (a * b) = f a * f b) : MulZeroClass M₀'

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)

ink

def Function.Surjective.mulZeroClass {M₀ : Type u_1} {M₀' : Type u_2} [inst : MulZeroClass M₀] [inst : Mul M₀'] [inst : Zero M₀'] (f : M₀ → M₀') (hf : Function.Surjective f) (zero : f 0 = 0) (mul : ∀ (a b : M₀), f (a * b) = f a * f b) : MulZeroClass M₀'

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)

ink

theorem Function.Injective.noZeroDivisors {M₀ : Type u_1} {M₀' : Type u_2} [inst : Mul M₀] [inst : Zero M₀] [inst : Mul M₀'] [inst : Zero M₀'] [inst : NoZeroDivisors M₀'] (f : M₀ → M₀') (hf : Function.Injective f) (zero : f 0 = 0) (mul : ∀ (x y : M₀), f (x * y) = f x * f y) : NoZeroDivisors M₀

Pushforward a NoZeroDivisors instance along an injective function.

ink

def Function.Injective.mulZeroOneClass {M₀ : Type u_1} {M₀' : Type u_2} [inst : MulZeroOneClass M₀] [inst : Mul M₀'] [inst : Zero M₀'] [inst : One M₀'] (f : M₀' → M₀) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (a b : M₀'), f (a * b) = f a * f b) : MulZeroOneClass M₀'

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.

ink

def Function.Surjective.mulZeroOneClass {M₀ : Type u_1} {M₀' : Type u_2} [inst : MulZeroOneClass M₀] [inst : Mul M₀'] [inst : Zero M₀'] [inst : One M₀'] (f : M₀ → M₀') (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (a b : M₀), f (a * b) = f a * f b) : MulZeroOneClass M₀'

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.

ink

def Function.Injective.semigroupWithZero {M₀ : Type u_1} {M₀' : Type u_2} [inst : Zero M₀'] [inst : Mul M₀'] [inst : SemigroupWithZero M₀] (f : M₀' → M₀) (hf : Function.Injective f) (zero : f 0 = 0) (mul : ∀ (x y : M₀'), f (x * y) = f x * f y) : SemigroupWithZero M₀'

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.

ink

def Function.Surjective.semigroupWithZero {M₀ : Type u_1} {M₀' : Type u_2} [inst : SemigroupWithZero M₀] [inst : Zero M₀'] [inst : Mul M₀'] (f : M₀ → M₀') (hf : Function.Surjective f) (zero : f 0 = 0) (mul : ∀ (x y : M₀), f (x * y) = f x * f y) : SemigroupWithZero M₀'

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.

ink

def Function.Injective.monoidWithZero {M₀ : Type u_1} {M₀' : Type u_2} [inst : Zero M₀'] [inst : Mul M₀'] [inst : One M₀'] [inst : Pow M₀' ℕ] [inst : MonoidWithZero M₀] (f : M₀' → M₀) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀'), f (x * y) = f x * f y) (npow : ∀ (x : M₀') (n : ℕ), f (x ^ n) = f x ^ n) : MonoidWithZero M₀'

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.

ink

def Function.Surjective.monoidWithZero {M₀ : Type u_1} {M₀' : Type u_2} [inst : Zero M₀'] [inst : Mul M₀'] [inst : One M₀'] [inst : Pow M₀' ℕ] [inst : MonoidWithZero M₀] (f : M₀ → M₀') (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀), f (x * y) = f x * f y) (npow : ∀ (x : M₀) (n : ℕ), f (x ^ n) = f x ^ n) : MonoidWithZero M₀'

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.

ink

def Function.Injective.commMonoidWithZero {M₀ : Type u_1} {M₀' : Type u_2} [inst : Zero M₀'] [inst : Mul M₀'] [inst : One M₀'] [inst : Pow M₀' ℕ] [inst : CommMonoidWithZero M₀] (f : M₀' → M₀) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀'), f (x * y) = f x * f y) (npow : ∀ (x : M₀') (n : ℕ), f (x ^ n) = f x ^ n) : CommMonoidWithZero M₀'

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.

ink

def Function.Surjective.commMonoidWithZero {M₀ : Type u_1} {M₀' : Type u_2} [inst : Zero M₀'] [inst : Mul M₀'] [inst : One M₀'] [inst : Pow M₀' ℕ] [inst : CommMonoidWithZero M₀] (f : M₀ → M₀') (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀), f (x * y) = f x * f y) (npow : ∀ (x : M₀) (n : ℕ), f (x ^ n) = f x ^ n) : CommMonoidWithZero M₀'

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.

ink

def Function.Injective.cancelMonoidWithZero {M₀ : Type u_1} {M₀' : Type u_2} [inst : CancelMonoidWithZero M₀] [inst : Zero M₀'] [inst : Mul M₀'] [inst : One M₀'] [inst : Pow M₀' ℕ] (f : M₀' → M₀) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀'), f (x * y) = f x * f y) (npow : ∀ (x : M₀') (n : ℕ), f (x ^ n) = f x ^ n) : CancelMonoidWithZero M₀'

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.

ink

def Function.Injective.cancelCommMonoidWithZero {M₀ : Type u_1} {M₀' : Type u_2} [inst : CancelCommMonoidWithZero M₀] [inst : Zero M₀'] [inst : Mul M₀'] [inst : One M₀'] [inst : Pow M₀' ℕ] (f : M₀' → M₀) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀'), f (x * y) = f x * f y) (npow : ∀ (x : M₀') (n : ℕ), f (x ^ n) = f x ^ n) : CancelCommMonoidWithZero M₀'

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.

ink

def Function.Injective.groupWithZero {G₀ : Type u_1} {G₀' : Type u_2} [inst : GroupWithZero G₀] [inst : Zero G₀'] [inst : Mul G₀'] [inst : One G₀'] [inst : Inv G₀'] [inst : Div G₀'] [inst : Pow G₀' ℕ] [inst : Pow G₀' ℤ] (f : G₀' → G₀) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : G₀'), f (x * y) = f x * f y) (inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : G₀'), f (x / y) = f x / f y) (npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n) : GroupWithZero G₀'

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.

ink

def Function.Surjective.groupWithZero {G₀ : Type u_1} {G₀' : Type u_2} [inst : GroupWithZero G₀] [inst : Zero G₀'] [inst : Mul G₀'] [inst : One G₀'] [inst : Inv G₀'] [inst : Div G₀'] [inst : Pow G₀' ℕ] [inst : Pow G₀' ℤ] (h01 : 0 ≠ 1) (f : G₀ → G₀') (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : G₀), f (x * y) = f x * f y) (inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : G₀), f (x / y) = f x / f y) (npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n) : GroupWithZero G₀'

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.

ink

def Function.Injective.commGroupWithZero {G₀ : Type u_1} {G₀' : Type u_2} [inst : CommGroupWithZero G₀] [inst : Zero G₀'] [inst : Mul G₀'] [inst : One G₀'] [inst : Inv G₀'] [inst : Div G₀'] [inst : Pow G₀' ℕ] [inst : Pow G₀' ℤ] (f : G₀' → G₀) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : G₀'), f (x * y) = f x * f y) (inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : G₀'), f (x / y) = f x / f y) (npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n) : CommGroupWithZero G₀'

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.

ink

def Function.Surjective.commGroupWithZero {G₀ : Type u_1} {G₀' : Type u_2} [inst : CommGroupWithZero G₀] [inst : Zero G₀'] [inst : Mul G₀'] [inst : One G₀'] [inst : Inv G₀'] [inst : Div G₀'] [inst : Pow G₀' ℕ] [inst : Pow G₀' ℤ] (h01 : 0 ≠ 1) (f : G₀ → G₀') (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : G₀), f (x * y) = f x * f y) (inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : G₀), f (x / y) = f x / f y) (npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n) : CommGroupWithZero G₀'

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.