Commit 2026-10-17 19:24 3dfb8e22

View on Github →

chore: remove WittVector.mk' (#43374) Override the structure constructor transparencies so that duplicating a WittVector.mk' is no longer necessary.

Estimated changes

Modified Mathlib/RingTheory/WittVector/Defs.lean

added def WittVector.mk'

deleted def WittVector.mk

modified structure WittVector

Modified Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean

Modified Mathlib/RingTheory/WittVector/Domain.lean

Modified Mathlib/RingTheory/WittVector/Frobenius.lean

Modified Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean

Modified Mathlib/RingTheory/WittVector/InitTail.lean

Modified Mathlib/RingTheory/WittVector/IsPoly.lean

Modified Mathlib/RingTheory/WittVector/Teichmuller.lean

Modified Mathlib/RingTheory/WittVector/Truncated.lean

Modified Mathlib/RingTheory/WittVector/Verschiebung.lean