精益：定义R理想和R模块的乘积

Question

我正在尝试学习精益，并且试图弄清楚如何I*M = {i*m | i in I, m in M}从理想的I和R模块M 创建新的R模块。

因此，我的尝试是首先定义一个映射ideal_mult，该映射将创建一个新的R模块，然后弄清楚如何为其分配一个好的符号。

import ring_theory.ideals
import algebra.module

universes u v
variables {R : Type u} {M : Type v}
variables [comm_ring R] [add_comm_group M] [module R M]
variables (I: ideal R)

def ideal_mult (I: ideal R) (M: Type v)
        [add_comm_group M] [module R M]: Type v
        :=
    sorry

#check ideal_mult I M

我该如何定义它，以便例如举例说明一个假设(h: I*M = M)？

感谢您的帮助！

Answer 1

你应该import ring_theory.ideal_operations。它具有您想要的定义，网址为https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/ideal_operations.lean#L556

然后I • ?，您可以输入产品（•在VScode-lean中，=“ \ bullet”，也?=“ \ top”，它是Mie 的最大子模块，即您可以将其视为M自身）。你的假设会变成I • ? = ?。