Theorems · Theorem · commutative algebra

MvPolynomial.IsHomogeneous.funext_of_le_card

∀ {R : Type u_5} {σ : Type u_6} [inst : CommRing R] [IsDomain R] {F G : MvPolynomial σ R} {n : ℕ},
  F.IsHomogeneous n →
    G.IsHomogeneous n → (∀ (r : σ → R), (MvPolynomial.eval r) F = (MvPolynomial.eval r) G) → ↑n ≤ Cardinal.mk R → F = G

See MvPolynomial.IsHomogeneous.funext for a version that assumes Infinite R.

Defined in

Mathlib.RingTheory.MvPolynomial.Homogeneous

Cited by

1 results in Mathlib

Foundations

Depth 139 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomain