半环，即配备加法、乘法以及自然数到该类型的映射，并满足相应相容性条件的类型。
若该类型还带有取负运算，请改用 Ring；若乘法可交换，请改用 CommSemiring；若既有取负运算且乘法可交换，请改用 CommRing。
实例构造子
Lean.Grind.Semiring.mk.{u}
扩展
方法
add : α → α → α
继承自父结构。
mul : α → α → α
继承自父结构。
natCast : NatCast α
每个半环中都有从自然数到该半环的典范映射，它给出 0 和 1 的值。注意，此函数不一定是单射。
ofNat : (n : Nat) → OfNat α n
半环中的自然数数值。字段 ofNat_eq_natCast 保证它们在命题意义下等于 natCast 的值。
nsmul : SMul Nat α
自然数标量乘法。
npow : HPow α Nat α
自然数幂运算。
add_zero : ∀ (a : α), a + 0 = a
零是加法右单位元。
add_comm : ∀ (a b : α), a + b = b + a
加法可交换。
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
加法满足结合律。
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
乘法满足结合律。
mul_one : ∀ (a : α), a * 1 = a
一是乘法右单位元。
one_mul : ∀ (a : α), 1 * a = a
一是乘法左单位元。
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
乘法对加法满足左分配律。
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
乘法对加法满足右分配律。
zero_mul : ∀ (a : α), 0 * a = 0
零对乘法具有右吸收性。
mul_zero : ∀ (a : α), a * 0 = 0
零对乘法具有左吸收性。
pow_zero : ∀ (a : α), a ^ 0 = 1
任意元素的零次幂为一。
pow_succ : ∀ (a : α) (n : Nat), a ^ (n + 1) = a ^ n * a
幂运算的后继律。
ofNat_succ : ∀ (a : Nat), OfNat.ofNat (a + 1) = OfNat.ofNat a + 1
数值与加法的定义相容。
ofNat_eq_natCast : ∀ (n : Nat), OfNat.ofNat n = ↑n
数值与自然数的典范映射相容。
nsmul_eq_natCast_mul : ∀ (n : Nat) (a : α), n • a = ↑n * a
乘以数值与自然数的典范映射相容。