equivNum_apply — Mathlib

English

The application of the equivalence equivNum on an element x is given by algebraic action with the denominator.

Русский

Применение эквивалентности equivNum к элементу x задаётся действием по знаменателю.

LaTeX

$$$equivNum\\, h_nz\\, x \\text{ maps to } a \\cdot x$, with $a= I.den$$$

Lean4

@[simp]
theorem equivNum_apply [Nontrivial P] [NoZeroSMulDivisors R P] {I : FractionalIdeal S P} (h_nz : (I.den : R) ≠ 0)
    (x : I) : algebraMap R P (equivNum h_nz x) = I.den • x :=
  by
  change Algebra.linearMap R P _ = _
  rw [equivNum, LinearEquiv.trans_apply, LinearEquiv.ofBijective_apply, LinearMap.restrict_apply,
    Submodule.map_equivMapOfInjective_symm_apply, Subtype.coe_mk, DistribMulAction.toLinearMap_apply]

Похожие утверждения